Beginning of Section Topology
Definition. We define
open_in to be
λX T U ⇒ topology_on X T ∧ U ∈ T of type
set → set → set → prop .
Proof: Let X be given.
Let T be given.
Let U be given.
Assume Htop HU .
Apply andI to the current goal.
An exact proof term for the current goal is Htop .
Apply andI to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU .
∎
Definition. We define
finer_than to be
λT' T ⇒ T ⊆ T' of type
set → set → prop .
Definition. We define
coarser_than to be
λT' T ⇒ T' ⊆ T of type
set → set → prop .
Proof: Let X be given.
Assume Hfin .
Apply Hfin to the current goal.
Let n be given.
We prove the intermediate
claim Hn :
n ∈ ω .
An
exact proof term for the current goal is
(andEL (n ∈ ω ) (equip X n ) Hpair ) .
We prove the intermediate
claim Heq :
equip X n .
An
exact proof term for the current goal is
(andER (n ∈ ω ) (equip X n ) Hpair ) .
We prove the intermediate
claim Hn_sub :
n ⊆ ω .
We prove the intermediate
claim Hcount_n :
atleastp n ω .
An
exact proof term for the current goal is
(Subq_atleastp n ω Hn_sub ) .
We prove the intermediate
claim Hcount_X :
atleastp X n .
An
exact proof term for the current goal is
(atleastp_tra X n ω Hcount_X Hcount_n ) .
∎
Proof: Let X and Y be given.
Assume HcountY HsubXY .
An
exact proof term for the current goal is
(Subq_atleastp X Y HsubXY ) .
An exact proof term for the current goal is HcountY .
∎
Axiom. (
Union_Power ) We take the following as an axiom:
∀X Fam : set , Fam ⊆ 𝒫 X → ⋃ Fam ⊆ X
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An
exact proof term for the current goal is
(Subq_ref (𝒫 X ) ) .
Apply PowerI to the current goal.
An
exact proof term for the current goal is
(Subq_ref X ) .
We will
prove ∀UFam ∈ 𝒫 (𝒫 X ) , ⋃ UFam ∈ 𝒫 X .
Let UFam be given.
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Let U be given.
We prove the intermediate
claim HFamSub :
UFam ⊆ 𝒫 X .
An
exact proof term for the current goal is
(iffEL (UFam ∈ 𝒫 (𝒫 X ) ) (UFam ⊆ 𝒫 X ) (PowerEq (𝒫 X ) UFam ) Hfam ) .
We prove the intermediate
claim HUinPower :
U ∈ 𝒫 X .
An exact proof term for the current goal is HFamSub U HUinFam .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(iffEL (U ∈ 𝒫 X ) (U ⊆ X ) (PowerEq X U ) HUinPower ) .
An exact proof term for the current goal is (HUsub x HUinx ) .
We will
prove ∀U ∈ 𝒫 X , ∀V ∈ 𝒫 X , U ∩ V ∈ 𝒫 X .
Let U be given.
Let V be given.
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxU HxV .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(iffEL (U ∈ 𝒫 X ) (U ⊆ X ) (PowerEq X U ) HU ) .
An exact proof term for the current goal is (HUsub x HxU ) .
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
rewrite the current goal using HUe (from left to right).
rewrite the current goal using HUX (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
Let UFam be given.
Apply xm (∃U : set , U ∈ UFam ∧ U = X ) to the current goal.
We prove the intermediate
claim HUnion_sub :
⋃ UFam ⊆ X .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (Hsub U HUin ) .
We prove the intermediate
claim HxEmpty :
x ∈ Empty .
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(EmptyE x HxEmpty (x ∈ X ) ) .
rewrite the current goal using HUX (from right to left).
An exact proof term for the current goal is HxU .
We prove the intermediate
claim HX_sub :
X ⊆ ⋃ UFam .
Let x be given.
Assume HxX .
Apply Hex to the current goal.
Let U be given.
We prove the intermediate
claim HUin :
U ∈ UFam .
An
exact proof term for the current goal is
(andEL (U ∈ UFam ) (U = X ) HUinpair ) .
We prove the intermediate
claim HUeq :
U = X .
An
exact proof term for the current goal is
(andER (U ∈ UFam ) (U = X ) HUinpair ) .
We prove the intermediate
claim HxU :
x ∈ U .
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxX .
Apply UnionI UFam x U HxU HUin to the current goal.
We prove the intermediate
claim HUnion_eq :
⋃ UFam = X .
An exact proof term for the current goal is HUnion_sub .
An exact proof term for the current goal is HX_sub .
rewrite the current goal using HUnion_eq (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
We prove the intermediate
claim HUnion_empty :
⋃ UFam = Empty .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (Hsub U HUin ) .
We prove the intermediate
claim HxEmpty :
x ∈ Empty .
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU .
An exact proof term for the current goal is HxEmpty .
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin .
An exact proof term for the current goal is HUX .
rewrite the current goal using HUnion_empty (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
Let U be given.
Let V be given.
We prove the intermediate
claim Hcap :
U ∩ V = Empty .
rewrite the current goal using HUe (from left to right).
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
We prove the intermediate
claim Hcap :
U ∩ V = Empty .
rewrite the current goal using HVe (from left to right).
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
We prove the intermediate
claim Hcap :
U ∩ V = X .
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
Let x be given.
Assume HxX .
rewrite the current goal using HUX (from left to right).
rewrite the current goal using HVX (from left to right).
An
exact proof term for the current goal is
(binintersectI X X x HxX HxX ) .
rewrite the current goal using Hcap (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX ) .
We prove the intermediate
claim HfinDiff :
finite (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
Let UFam be given.
Apply xm (∃U : set , U ∈ UFam ∧ finite (X ∖ U ) ) to the current goal.
We prove the intermediate
claim HUnionInPower :
⋃ UFam ∈ 𝒫 X .
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
We prove the intermediate
claim HUinPow :
U ∈ 𝒫 X .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U (Hsub U HUin ) ) .
We prove the intermediate
claim HUsub :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U HUinPow ) .
An exact proof term for the current goal is (HUsub x HxU ) .
We prove the intermediate
claim HUnionPred :
finite (X ∖ ⋃ UFam ) ∨ ⋃ UFam = Empty .
Apply orIL to the current goal.
Apply Hex to the current goal.
Let U be given.
We prove the intermediate
claim HUin :
U ∈ UFam .
An
exact proof term for the current goal is
(andEL (U ∈ UFam ) (finite (X ∖ U ) ) Hpair ) .
We prove the intermediate
claim HUfin :
finite (X ∖ U ) .
An
exact proof term for the current goal is
(andER (U ∈ UFam ) (finite (X ∖ U ) ) Hpair ) .
We prove the intermediate
claim Hsubset :
X ∖ ⋃ UFam ⊆ X ∖ U .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (⋃ UFam ) x Hx ) .
We prove the intermediate
claim HnotUnion :
x ∉ ⋃ UFam .
An
exact proof term for the current goal is
(setminusE2 X (⋃ UFam ) x Hx ) .
We prove the intermediate
claim HnotU :
x ∉ U .
Assume HxU .
Apply HnotUnion to the current goal.
Apply UnionI UFam x U HxU HUin to the current goal.
Apply setminusI X U x HxX HnotU to the current goal.
An
exact proof term for the current goal is
(Subq_finite (X ∖ U ) HUfin (X ∖ ⋃ UFam ) Hsubset ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) (⋃ UFam ) HUnionInPower HUnionPred ) .
We prove the intermediate
claim HUnionEmpty :
⋃ UFam = Empty .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U (Hsub U HUin ) ) .
Apply HUdata (x ∈ Empty ) to the current goal.
Assume HUfin .
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin .
An exact proof term for the current goal is HUfin .
rewrite the current goal using HUempty (from right to left).
An exact proof term for the current goal is HxU .
rewrite the current goal using HUnionEmpty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
Let U be given.
Let V be given.
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) V HV ) .
Assume HUfin .
Assume HVfin .
We prove the intermediate
claim HcapInPower :
U ∩ V ∈ 𝒫 X .
We prove the intermediate
claim HUsub :
U ⊆ X .
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxCap .
Assume HxU HxV .
An exact proof term for the current goal is (HUsub x HxU ) .
Apply orIL to the current goal.
We prove the intermediate
claim HfinUnion :
finite ((X ∖ U ) ∪ (X ∖ V ) ) .
An
exact proof term for the current goal is
(binunion_finite (X ∖ U ) HUfin (X ∖ V ) HVfin ) .
We prove the intermediate
claim Hsubset :
X ∖ (U ∩ V ) ⊆ (X ∖ U ) ∪ (X ∖ V ) .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (U ∩ V ) x Hx ) .
We prove the intermediate
claim HnotCap :
x ∉ U ∩ V .
An
exact proof term for the current goal is
(setminusE2 X (U ∩ V ) x Hx ) .
Apply xm (x ∈ U ) to the current goal.
Assume HxU .
We prove the intermediate
claim HnotV :
x ∉ V .
Assume HxV .
Apply HnotCap to the current goal.
An
exact proof term for the current goal is
(binintersectI U V x HxU HxV ) .
Apply setminusI X V x HxX HnotV to the current goal.
Assume HnotU .
Apply setminusI X U x HxX HnotU to the current goal.
An
exact proof term for the current goal is
(Subq_finite ((X ∖ U ) ∪ (X ∖ V ) ) HfinUnion (X ∖ (U ∩ V ) ) Hsubset ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) (U ∩ V ) HcapInPower HcapPred ) .
We prove the intermediate
claim Hcap_empty :
U ∩ V = Empty .
rewrite the current goal using HVempty (from left to right).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
We prove the intermediate
claim Hcap_empty :
U ∩ V = Empty .
rewrite the current goal using HUempty (from left to right).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen .
∎
Proof: Let T be given.
An
exact proof term for the current goal is
(Subq_ref T ) .
∎
Proof: Let A, B and C be given.
An
exact proof term for the current goal is
(Subq_tra A B C H1 H2 ) .
∎
Proof: Let T and T' be given.
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X, T1 and T2 be given.
Assume H .
We prove the intermediate
claim Heq :
T1 = T2 .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT2 .
An exact proof term for the current goal is HT1 .
rewrite the current goal using Heq (from right to left).
Use reflexivity.
∎
Proof: Let X, T1, T2 and T3 be given.
Assume H12 H23 .
We prove the intermediate
claim H12eq :
T1 = T2 .
We prove the intermediate
claim H23eq :
T2 = T3 .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT1 .
An exact proof term for the current goal is HT3 .
rewrite the current goal using H12eq (from left to right).
rewrite the current goal using H23eq (from left to right).
Use reflexivity.
∎
Proof: Let X and T be given.
Assume HT .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT .
An exact proof term for the current goal is HT .
∎
Proof: Let T and T' be given.
Apply iffI to the current goal.
Assume H .
An exact proof term for the current goal is H .
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X and T be given.
Assume HT .
We prove the intermediate
claim H1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim H2 :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) H1 ) .
We prove the intermediate
claim H3 :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) H2 ) .
We prove the intermediate
claim HTsub :
T ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ) (Empty ∈ T ) H3 ) .
An exact proof term for the current goal is HTsub .
∎
Proof: Let X and T be given.
Assume HT .
We prove the intermediate
claim Hchunk1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim Hchunk2 :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hchunk1 ) .
We prove the intermediate
claim Hchunk3 :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hchunk2 ) .
We prove the intermediate
claim Hempty :
Empty ∈ T .
An
exact proof term for the current goal is
(andER (T ⊆ 𝒫 X ) (Empty ∈ T ) Hchunk3 ) .
We prove the intermediate
claim HX :
X ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ) ∧ Empty ∈ T ) (X ∈ T ) Hchunk2 ) .
Let U be given.
rewrite the current goal using HUempty (from left to right).
An exact proof term for the current goal is Hempty .
rewrite the current goal using HUX (from left to right).
An exact proof term for the current goal is HX .
∎
Proof: Let X and U be given.
Assume HUsub .
Apply PowerI X U HUsub to the current goal.
∎
Proof: Let X and U be given.
Apply iffI to the current goal.
Assume HU .
An
exact proof term for the current goal is
(UPairE U Empty X HU ) .
rewrite the current goal using HUE (from left to right).
An
exact proof term for the current goal is
(UPairI1 Empty X ) .
rewrite the current goal using HUX (from left to right).
An
exact proof term for the current goal is
(UPairI2 Empty X ) .
An
exact proof term for the current goal is
(Hcases (U ∈ indiscrete_topology X ) HUempty_branch HUx_branch ) .
∎
Proof: Let X and U be given.
Assume Hopen .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HUin ) .
∎
Proof: Let X be given.
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim Hxin :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot Hxin ) .
We prove the intermediate
claim HfinDiff :
finite (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
∎
Proof: Let X and U be given.
Assume Hopen .
∎
Proof: Let X be given.
We prove the intermediate
claim Hdiff_empty :
X ∖ X = Empty .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X X x Hx ) .
We prove the intermediate
claim Hxnot :
x ∉ X .
An
exact proof term for the current goal is
(setminusE2 X X x Hx ) .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX ) .
We prove the intermediate
claim HcountDiff :
countable (X ∖ X ) .
rewrite the current goal using Hdiff_empty (from left to right).
∎
Proof: Let X be given.
Let U be given.
We prove the intermediate
claim HUinPow :
U ∈ 𝒫 X .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is HUemp .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ countable (X ∖ U0 ) ∨ U0 = Empty ) U HUinPow HUpred ) .
∎
Proof: Let X be given.
Let U be given.
Assume HU .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ finite (X ∖ U0 ) ∨ U0 = Empty ) U HU ) .
∎
Proof: Let X be given.
Let U be given.
rewrite the current goal using HUempty (from left to right).
rewrite the current goal using HUX (from left to right).
∎
Proof: Let X, T' and T be given.
Apply iffI to the current goal.
Assume H .
An exact proof term for the current goal is H .
Assume H .
An exact proof term for the current goal is H .
∎
Proof: Let X, T and UFam be given.
Assume HT Hfam .
We prove the intermediate
claim Hchunk1 :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) HT ) .
We prove the intermediate
claim Hunion_axiom :
∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam' ∈ 𝒫 T , ⋃ UFam' ∈ T ) Hchunk1 ) .
An exact proof term for the current goal is (Hunion_axiom UFam Hfam ) .
∎
Proof: Let X, T, U and V be given.
Assume HT HU HV .
We prove the intermediate
claim Hax_inter :
∀U' ∈ T , ∀V' ∈ T , U' ∩ V' ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ∧ X ∈ T ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) ) (∀U' ∈ T , ∀V' ∈ T , U' ∩ V' ∈ T ) HT ) .
An exact proof term for the current goal is (Hax_inter U HU V HV ) .
∎
Definition. We define
open_set_family to be
λ_ T ⇒ T of type
set → set → set .
Definition. We define
basis_on to be
λX B ⇒ B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ∧ (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) of type
set → set → prop .
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBleft :
B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
We prove the intermediate
claim HBint :
∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) HBleft ) .
We prove the intermediate
claim HBcov :
∀x ∈ X , ∃b ∈ B , x ∈ b .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) HBleft ) .
Let U be given.
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) U HU ) .
We prove the intermediate
claim HXprop :
∀x ∈ X , ∃b ∈ B , x ∈ b ∧ b ⊆ X .
Let x be given.
Assume HxX .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b .
An exact proof term for the current goal is (HBcov x HxX ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ) Hbpair ) .
We prove the intermediate
claim HbsubX :
b ⊆ X .
An
exact proof term for the current goal is
(PowerE X b (HBsub b HbB ) ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
An exact proof term for the current goal is HbsubX .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) X (Self_In_Power X ) HXprop ) .
Let UFam be given.
We prove the intermediate
claim HPowUnion :
⋃ UFam ∈ 𝒫 X .
Apply PowerI X (⋃ UFam ) to the current goal.
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (HsubFam U HUin ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) ) .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HUnionProp :
∀x ∈ ⋃ UFam , ∃b ∈ B , x ∈ b ∧ b ⊆ ⋃ UFam .
Let x be given.
Assume HxUnion .
Let U be given.
Assume HxU HUin .
An exact proof term for the current goal is (HsubFam U HUin ) .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbSubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
Let y be given.
Assume Hyb .
Apply UnionI UFam y U (HbSubU y Hyb ) HUin to the current goal.
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) (⋃ UFam ) HPowUnion HUnionProp ) .
Let U be given.
Assume HUtop .
Let V be given.
Assume HVtop .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
We prove the intermediate
claim HVprop :
∀x0 ∈ V , ∃b ∈ B , x0 ∈ b ∧ b ⊆ V .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) V HVtop ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) ) .
We prove the intermediate
claim HPowCap :
U ∩ V ∈ 𝒫 X .
Apply PowerI X (U ∩ V ) to the current goal.
Let x be given.
Assume HxCap .
Assume HxU HxV .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HCapProp :
∀x ∈ U ∩ V , ∃b ∈ B , x ∈ b ∧ b ⊆ U ∩ V .
Let x be given.
Assume HxCap .
Assume HxU HxV .
We prove the intermediate
claim Hexb1 :
∃b1 ∈ B , x ∈ b1 ∧ b1 ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
We prove the intermediate
claim Hexb2 :
∃b2 ∈ B , x ∈ b2 ∧ b2 ⊆ V .
An exact proof term for the current goal is (HVprop x HxV ) .
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hbpair1 .
We prove the intermediate
claim Hb1 :
b1 ∈ B .
An
exact proof term for the current goal is
(andEL (b1 ∈ B ) (x ∈ b1 ∧ b1 ⊆ U ) Hbpair1 ) .
We prove the intermediate
claim Hb1prop :
x ∈ b1 ∧ b1 ⊆ U .
An
exact proof term for the current goal is
(andER (b1 ∈ B ) (x ∈ b1 ∧ b1 ⊆ U ) Hbpair1 ) .
We prove the intermediate
claim Hb1x :
x ∈ b1 .
An
exact proof term for the current goal is
(andEL (x ∈ b1 ) (b1 ⊆ U ) Hb1prop ) .
We prove the intermediate
claim Hb1Sub :
b1 ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b1 ) (b1 ⊆ U ) Hb1prop ) .
Apply Hexb2 to the current goal.
Let b2 be given.
Assume Hbpair2 .
We prove the intermediate
claim Hb2 :
b2 ∈ B .
An
exact proof term for the current goal is
(andEL (b2 ∈ B ) (x ∈ b2 ∧ b2 ⊆ V ) Hbpair2 ) .
We prove the intermediate
claim Hb2prop :
x ∈ b2 ∧ b2 ⊆ V .
An
exact proof term for the current goal is
(andER (b2 ∈ B ) (x ∈ b2 ∧ b2 ⊆ V ) Hbpair2 ) .
We prove the intermediate
claim Hb2x :
x ∈ b2 .
An
exact proof term for the current goal is
(andEL (x ∈ b2 ) (b2 ⊆ V ) Hb2prop ) .
We prove the intermediate
claim Hb2Sub :
b2 ⊆ V .
An
exact proof term for the current goal is
(andER (x ∈ b2 ) (b2 ⊆ V ) Hb2prop ) .
We prove the intermediate
claim Hexb3 :
∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An exact proof term for the current goal is (HBint b1 Hb1 b2 Hb2 x Hb1x Hb2x ) .
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hbpair3 .
We prove the intermediate
claim Hb3 :
b3 ∈ B .
An
exact proof term for the current goal is
(andEL (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) Hbpair3 ) .
We prove the intermediate
claim Hb3prop :
x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) Hbpair3 ) .
We prove the intermediate
claim HxB3 :
x ∈ b3 .
An
exact proof term for the current goal is
(andEL (x ∈ b3 ) (b3 ⊆ b1 ∩ b2 ) Hb3prop ) .
We prove the intermediate
claim Hb3Sub :
b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (x ∈ b3 ) (b3 ⊆ b1 ∩ b2 ) Hb3prop ) .
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3 .
Apply andI to the current goal.
An exact proof term for the current goal is HxB3 .
Let y be given.
Assume Hyb3 .
We prove the intermediate
claim Hy_in_b1b2 :
y ∈ b1 ∩ b2 .
An exact proof term for the current goal is (Hb3Sub y Hyb3 ) .
Assume Hyb1 Hyb2 .
Apply binintersectI U V y (Hb1Sub y Hyb1 ) (Hb2Sub y Hyb2 ) to the current goal.
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) (U ∩ V ) HPowCap HCapProp ) .
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is proofA .
An exact proof term for the current goal is proofB .
An exact proof term for the current goal is proofC .
An exact proof term for the current goal is proofD .
An exact proof term for the current goal is proofE .
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
We prove the intermediate
claim HBint :
∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 .
An
exact proof term for the current goal is
(andER (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) .
Let b0 be given.
Assume Hb0 .
We prove the intermediate
claim Hb0_subX :
b0 ⊆ X .
An
exact proof term for the current goal is
(PowerE X b0 (HBsub b0 Hb0 ) ) .
We prove the intermediate
claim Hb0prop :
∀x ∈ b0 , ∃b ∈ B , x ∈ b ∧ b ⊆ b0 .
Let x be given.
Assume Hxb0 .
We prove the intermediate
claim Hexb3 :
∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 .
An exact proof term for the current goal is (HBint b0 Hb0 b0 Hb0 x Hxb0 Hxb0 ) .
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3pair .
We prove the intermediate
claim Hb3 :
b3 ∈ B .
An
exact proof term for the current goal is
(andEL (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 ) Hb3pair ) .
We prove the intermediate
claim Hb3prop :
x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 .
An
exact proof term for the current goal is
(andER (b3 ∈ B ) (x ∈ b3 ∧ b3 ⊆ b0 ∩ b0 ) Hb3pair ) .
We prove the intermediate
claim Hxb3 :
x ∈ b3 .
An
exact proof term for the current goal is
(andEL (x ∈ b3 ) (b3 ⊆ b0 ∩ b0 ) Hb3prop ) .
We prove the intermediate
claim Hb3sub_inter :
b3 ⊆ b0 ∩ b0 .
An
exact proof term for the current goal is
(andER (x ∈ b3 ) (b3 ⊆ b0 ∩ b0 ) Hb3prop ) .
We prove the intermediate
claim Hb3subb0 :
b3 ⊆ b0 .
Let y be given.
Assume Hyb3 .
We prove the intermediate
claim Hycap :
y ∈ b0 ∩ b0 .
An exact proof term for the current goal is (Hb3sub_inter y Hyb3 ) .
Assume Hy1 Hy2 .
An exact proof term for the current goal is Hy1 .
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3 .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb3 .
An exact proof term for the current goal is Hb3subb0 .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x ∈ U0 , ∃b ∈ B , x ∈ b ∧ b ⊆ U0 ) b0 (PowerI X b0 Hb0_subX ) Hb0prop ) .
∎
Proof: Let X and B be given.
Assume HBasis .
Use reflexivity.
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
Let U be given.
Assume HUopen .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
Apply PowerI B Fam to the current goal.
Let b be given.
Assume HbFam .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
We prove the intermediate
claim HUnion_eq :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
We use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow .
An exact proof term for the current goal is HUnion_eq .
∎
Proof: Let X and B be given.
Assume HBasis .
We prove the intermediate
claim HBsub :
B ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ) (∀x ∈ X , ∃b ∈ B , x ∈ b ) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X , ∃b ∈ B , x ∈ b ) ) (∀b1 ∈ B , ∀b2 ∈ B , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ B , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) HBasis ) ) .
Let U be given.
Assume Hex .
Apply Hex to the current goal.
Let Fam be given.
Assume HFampair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnionEq :
⋃ Fam = U .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HFamSubB :
Fam ⊆ B .
An
exact proof term for the current goal is
(PowerE B Fam HFamPow ) .
We prove the intermediate
claim HFamSubX :
Fam ⊆ 𝒫 X .
Let b be given.
Assume HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An exact proof term for the current goal is (HFamSubB b HbFam ) .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HUnionSubX :
⋃ Fam ⊆ X .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbSubX :
b ⊆ X .
An
exact proof term for the current goal is
(PowerE X b (HFamSubX b HbFam ) ) .
An exact proof term for the current goal is (HbSubX x Hxb ) .
We prove the intermediate
claim HUnionSubU :
⋃ Fam ⊆ U .
rewrite the current goal using HUnionEq (from left to right).
An
exact proof term for the current goal is
(Subq_ref U ) .
We prove the intermediate
claim HUsubUnion :
U ⊆ ⋃ Fam .
rewrite the current goal using HUnionEq (from right to left).
An
exact proof term for the current goal is
(Subq_ref (⋃ Fam ) ) .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(Subq_tra U (⋃ Fam ) X HUsubUnion HUnionSubX ) .
We prove the intermediate
claim HUpropU :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
Let x be given.
Assume HxU .
We prove the intermediate
claim HxUnion :
x ∈ ⋃ Fam .
An exact proof term for the current goal is (HUsubUnion x HxU ) .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An exact proof term for the current goal is (HFamSubB b HbFam ) .
We prove the intermediate
claim HbSubUnion :
b ⊆ ⋃ Fam .
Let y be given.
Assume Hyb .
An
exact proof term for the current goal is
(UnionI Fam y b Hyb HbFam ) .
We prove the intermediate
claim HbSubU :
b ⊆ U .
An
exact proof term for the current goal is
(Subq_tra b (⋃ Fam ) U HbSubUnion HUnionSubU ) .
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb .
An exact proof term for the current goal is HbSubU .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUpropU ) .
∎
Proof: Let X and B be given.
Assume HBasis .
Let U be given.
Assume HUopen .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HUtop ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
∎
Proof: Let X, T and C be given.
Assume Htop HCsub Href .
We prove the intermediate
claim Hleft :
((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) .
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) Htop ) .
We prove the intermediate
claim Hcore :
(T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T .
An
exact proof term for the current goal is
(andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hleft ) .
We prove the intermediate
claim HTPowEmpty :
T ⊆ 𝒫 X ∧ Empty ∈ T .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hcore ) .
We prove the intermediate
claim HTsubPow :
T ⊆ 𝒫 X .
An
exact proof term for the current goal is
(andEL (T ⊆ 𝒫 X ) (Empty ∈ T ) HTPowEmpty ) .
We prove the intermediate
claim HXT :
X ∈ T .
An
exact proof term for the current goal is
(andER (T ⊆ 𝒫 X ∧ Empty ∈ T ) (X ∈ T ) Hcore ) .
We prove the intermediate
claim HUnionClosed :
∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T .
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) Hleft ) .
We prove the intermediate
claim HInterClosed :
∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T .
An
exact proof term for the current goal is
(andER (((T ⊆ 𝒫 X ∧ Empty ∈ T ) ∧ X ∈ T ) ∧ (∀UFam ∈ 𝒫 T , ⋃ UFam ∈ T ) ) (∀U ∈ T , ∀V ∈ T , U ∩ V ∈ T ) Htop ) .
We prove the intermediate
claim HBasis :
basis_on X C .
We will
prove (C ⊆ 𝒫 X ∧ (∀x ∈ X , ∃c ∈ C , x ∈ c ) ∧ (∀b1 ∈ C , ∀b2 ∈ C , ∀x : set , x ∈ b1 → x ∈ b2 → ∃b3 ∈ C , x ∈ b3 ∧ b3 ⊆ b1 ∩ b2 ) ) .
Apply andI to the current goal.
Apply andI to the current goal.
Let c be given.
Assume HcC .
An exact proof term for the current goal is (HTsubPow c (HCsub c HcC ) ) .
Let x be given.
Assume HxX .
We prove the intermediate
claim Hex :
∃c ∈ C , x ∈ c ∧ c ⊆ X .
An exact proof term for the current goal is (Href X HXT x HxX ) .
Apply Hex to the current goal.
Let c be given.
Assume Hpair .
We prove the intermediate
claim HcC :
c ∈ C .
An
exact proof term for the current goal is
(andEL (c ∈ C ) (x ∈ c ∧ c ⊆ X ) Hpair ) .
We prove the intermediate
claim Hcprop :
x ∈ c ∧ c ⊆ X .
An
exact proof term for the current goal is
(andER (c ∈ C ) (x ∈ c ∧ c ⊆ X ) Hpair ) .
We prove the intermediate
claim Hxc :
x ∈ c .
An
exact proof term for the current goal is
(andEL (x ∈ c ) (c ⊆ X ) Hcprop ) .
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HcC .
An exact proof term for the current goal is Hxc .
Let c1 be given.
Assume Hc1C .
Let c2 be given.
Assume Hc2C .
Let x be given.
Assume Hxc1 Hxc2 .
We prove the intermediate
claim Hc1T :
c1 ∈ T .
An exact proof term for the current goal is (HCsub c1 Hc1C ) .
We prove the intermediate
claim Hc2T :
c2 ∈ T .
An exact proof term for the current goal is (HCsub c2 Hc2C ) .
We prove the intermediate
claim HcapT :
c1 ∩ c2 ∈ T .
An exact proof term for the current goal is (HInterClosed c1 Hc1T c2 Hc2T ) .
We prove the intermediate
claim HxCap :
x ∈ c1 ∩ c2 .
An
exact proof term for the current goal is
(binintersectI c1 c2 x Hxc1 Hxc2 ) .
We prove the intermediate
claim Hex :
∃c3 ∈ C , x ∈ c3 ∧ c3 ⊆ c1 ∩ c2 .
An
exact proof term for the current goal is
(Href (c1 ∩ c2 ) HcapT x HxCap ) .
An exact proof term for the current goal is Hex .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HUgen ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃c ∈ C , x ∈ c ∧ c ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HUgen ) .
Set Fam to be the term
{ c ∈ C | c ⊆ U } of type
set .
We prove the intermediate
claim HFamSubC :
Fam ⊆ C .
Let c be given.
Assume HcFam .
An
exact proof term for the current goal is
(SepE1 C (λc0 : set ⇒ c0 ⊆ U ) c HcFam ) .
We prove the intermediate
claim HFamSubT :
Fam ⊆ T .
Let c be given.
Assume HcFam .
We prove the intermediate
claim HcC :
c ∈ C .
An exact proof term for the current goal is (HFamSubC c HcFam ) .
An exact proof term for the current goal is (HCsub c HcC ) .
We prove the intermediate
claim HFamPowT :
Fam ∈ 𝒫 T .
An
exact proof term for the current goal is
(PowerI T Fam HFamSubT ) .
We prove the intermediate
claim HUnionSubU :
⋃ Fam ⊆ U .
Let x be given.
Assume HxUnion .
Let c be given.
Assume Hxc HcFam .
We prove the intermediate
claim Hcprop :
c ⊆ U .
An
exact proof term for the current goal is
(SepE2 C (λc0 : set ⇒ c0 ⊆ U ) c HcFam ) .
An exact proof term for the current goal is (Hcprop x Hxc ) .
We prove the intermediate
claim HUsubUnion :
U ⊆ ⋃ Fam .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hex :
∃c ∈ C , x ∈ c ∧ c ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hex to the current goal.
Let c be given.
Assume Hcpair .
We prove the intermediate
claim HcC :
c ∈ C .
An
exact proof term for the current goal is
(andEL (c ∈ C ) (x ∈ c ∧ c ⊆ U ) Hcpair ) .
We prove the intermediate
claim Hcprop :
x ∈ c ∧ c ⊆ U .
An
exact proof term for the current goal is
(andER (c ∈ C ) (x ∈ c ∧ c ⊆ U ) Hcpair ) .
We prove the intermediate
claim Hxc :
x ∈ c .
An
exact proof term for the current goal is
(andEL (x ∈ c ) (c ⊆ U ) Hcprop ) .
We prove the intermediate
claim HcsubU :
c ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ c ) (c ⊆ U ) Hcprop ) .
We prove the intermediate
claim HcFam :
c ∈ Fam .
An
exact proof term for the current goal is
(SepI C (λc0 : set ⇒ c0 ⊆ U ) c HcC HcsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x c Hxc HcFam ) .
We prove the intermediate
claim HUnionEqU :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
An exact proof term for the current goal is (HUnionSubU x HxUnion ) .
Let x be given.
Assume HxU .
An exact proof term for the current goal is (HUsubUnion x HxU ) .
We prove the intermediate
claim HUnionInT :
⋃ Fam ∈ T .
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT ) .
rewrite the current goal using HUnionEqU (from right to left).
An exact proof term for the current goal is HUnionInT .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (HTsubPow U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃c ∈ C , x ∈ c ∧ c ⊆ U .
Let x be given.
Assume HxU .
An exact proof term for the current goal is (Href U HU x HxU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ C , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
Let U be given.
Assume HUgen .
An exact proof term for the current goal is (Hgen_sub_T U HUgen ) .
Let U be given.
Assume HU .
An exact proof term for the current goal is (HT_sub_gen U HU ) .
Apply andI to the current goal.
An exact proof term for the current goal is HBasis .
An exact proof term for the current goal is HEqual .
∎
Proof: Let X, T and C be given.
Assume Htop HCsub Href .
∎
Proof: Let X, B and B' be given.
Assume HB HB' Hcond .
Let U be given.
Let x be given.
Assume HxU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HUsubX x HxU ) .
We prove the intermediate
claim HUprop :
∀x0 ∈ U , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ B , x0 ∈ b ∧ b ⊆ U0 ) U HU ) .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim Hexb' :
∃b' ∈ B' , x ∈ b' ∧ b' ⊆ b .
An exact proof term for the current goal is (Hcond x HxX b HbB Hxb ) .
Apply Hexb' to the current goal.
Let b' be given.
Assume Hb'pair .
We prove the intermediate
claim Hb'B :
b' ∈ B' .
An
exact proof term for the current goal is
(andEL (b' ∈ B' ) (x ∈ b' ∧ b' ⊆ b ) Hb'pair ) .
We prove the intermediate
claim Hb'prop :
x ∈ b' ∧ b' ⊆ b .
An
exact proof term for the current goal is
(andER (b' ∈ B' ) (x ∈ b' ∧ b' ⊆ b ) Hb'pair ) .
We prove the intermediate
claim Hxb' :
x ∈ b' .
An
exact proof term for the current goal is
(andEL (x ∈ b' ) (b' ⊆ b ) Hb'prop ) .
We prove the intermediate
claim Hb'subb :
b' ⊆ b .
An
exact proof term for the current goal is
(andER (x ∈ b' ) (b' ⊆ b ) Hb'prop ) .
We use b' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb'B .
Apply andI to the current goal.
An exact proof term for the current goal is Hxb' .
An
exact proof term for the current goal is
(Subq_tra b' b U Hb'subb HbsubU ) .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b' ∈ B' , x ∈ b' ∧ b' ⊆ U .
An exact proof term for the current goal is (HRefProp U HU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
∎
Proof: Let X, B and B' be given.
Assume HB HB' .
Apply iffI to the current goal.
Assume Hcond .
An
exact proof term for the current goal is
(finer_via_basis X B B' HB HB' Hcond ) .
Assume Hfiner .
Let x be given.
Assume HxX .
Let b be given.
Assume HbB Hxb .
An exact proof term for the current goal is (Hfiner b HbGen ) .
We prove the intermediate
claim Hbprop :
∀x0 ∈ b , ∃b' ∈ B' , x0 ∈ b' ∧ b' ⊆ b .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) b HbGen' ) .
An exact proof term for the current goal is (Hbprop x Hxb ) .
∎
Proof: Let X, B and T be given.
Assume HBasis HT HBsub .
We prove the intermediate
claim HUnionClosed :
∀Fam ∈ 𝒫 T , ⋃ Fam ∈ T .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b ∈ B , x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(SepE2 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) .
Set Fam to be the term
{ b ∈ B | b ⊆ U } of type
set .
We prove the intermediate
claim HFamPowB :
Fam ∈ 𝒫 B .
Apply PowerI B Fam to the current goal.
Let b be given.
Assume HbFam .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
We prove the intermediate
claim HUnionEq :
⋃ Fam = U .
Let x be given.
Assume HxUnion .
Let b be given.
Assume Hxb HbFam .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(SepE2 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HbsubU x Hxb ) .
Let x be given.
Assume HxU .
We prove the intermediate
claim Hexb :
∃b ∈ B , x ∈ b ∧ b ⊆ U .
An exact proof term for the current goal is (HUprop x HxU ) .
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(andEL (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hbprop :
x ∈ b ∧ b ⊆ U .
An
exact proof term for the current goal is
(andER (b ∈ B ) (x ∈ b ∧ b ⊆ U ) Hbpair ) .
We prove the intermediate
claim Hxb :
x ∈ b .
An
exact proof term for the current goal is
(andEL (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbsubU :
b ⊆ U .
An
exact proof term for the current goal is
(andER (x ∈ b ) (b ⊆ U ) Hbprop ) .
We prove the intermediate
claim HbT :
b ∈ T .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HbFam :
b ∈ Fam .
An
exact proof term for the current goal is
(SepI B (λb0 : set ⇒ b0 ⊆ U ) b HbB HbsubU ) .
An
exact proof term for the current goal is
(UnionI Fam x b Hxb HbFam ) .
We prove the intermediate
claim HFamPowT :
Fam ∈ 𝒫 T .
Apply PowerI T Fam to the current goal.
Let b be given.
Assume HbFam .
We prove the intermediate
claim HbB :
b ∈ B .
An
exact proof term for the current goal is
(SepE1 B (λb0 : set ⇒ b0 ⊆ U ) b HbFam ) .
An exact proof term for the current goal is (HBsub b HbB ) .
We prove the intermediate
claim HUnionT :
⋃ Fam ∈ T .
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT ) .
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionT .
∎
Proof: Let X, B and T be given.
Assume HBasis HT HBsub .
∎
Proof: Let X and B be given.
Assume HBasis .
Let U be given.
Assume HU .
We prove the intermediate
claim HexFam :
∃Fam ∈ 𝒫 B , ⋃ Fam = U .
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnion :
⋃ Fam = U .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (⋃ Fam = U ) HFampair ) .
We prove the intermediate
claim HUnionFam :
⋃ Fam ∈ { ⋃ Fam0 | Fam0 ∈ 𝒫 B } .
An
exact proof term for the current goal is
(ReplI (𝒫 B ) (λFam0 : set ⇒ ⋃ Fam0 ) Fam HFamPow ) .
rewrite the current goal using HUnion (from right to left).
An exact proof term for the current goal is HUnionFam .
Let U be given.
Assume HUUnion .
We prove the intermediate
claim HexFamPowRaw :
∃Fam ∈ 𝒫 B , U = ⋃ Fam .
An
exact proof term for the current goal is
(ReplE (𝒫 B ) (λFam0 : set ⇒ ⋃ Fam0 ) U HUUnion ) .
We prove the intermediate
claim HexFamPow :
∃Fam ∈ 𝒫 B , ⋃ Fam = U .
Apply HexFamPowRaw to the current goal.
Let Fam be given.
Assume HFamPair .
We prove the intermediate
claim HFamPow :
Fam ∈ 𝒫 B .
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B ) (U = ⋃ Fam ) HFamPair ) .
We prove the intermediate
claim HUnion :
U = ⋃ Fam .
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B ) (U = ⋃ Fam ) HFamPair ) .
We use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow .
rewrite the current goal using HUnion (from right to left).
Use reflexivity.
∎
Proof: Let X be given.
Apply andI to the current goal.
Apply andI to the current goal.
Let s be given.
Assume Hs .
Let x be given.
Assume HxX Hseq .
rewrite the current goal using Hseq (from left to right).
Apply PowerI to the current goal.
Let y be given.
Assume Hy .
Apply (UPairE y x x Hy (y ∈ X ) ) to the current goal.
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxX .
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxX .
Let x be given.
Assume HxX .
We use
{ x , x } to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(ReplI X (λx0 : set ⇒ { x0 , x0 } ) x HxX ) .
Let b1 be given.
Assume Hb1 .
Let b2 be given.
Assume Hb2 .
Let x be given.
Assume Hx1 Hx2 .
Let x1 be given.
Assume Hx1X Hb1eq .
Let x2 be given.
Assume Hx2X Hb2eq .
We prove the intermediate
claim Hx1in :
x ∈ { x1 , x1 } .
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1 .
We prove the intermediate
claim Hx2in :
x ∈ { x2 , x2 } .
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2 .
We prove the intermediate
claim Hx_eq_x1 :
x = x1 .
Apply (UPairE x x1 x1 Hx1in (x = x1 ) ) to the current goal.
Assume Hxx1 .
An exact proof term for the current goal is Hxx1 .
Assume Hxx1 .
An exact proof term for the current goal is Hxx1 .
We prove the intermediate
claim Hx_eq_x2 :
x = x2 .
Apply (UPairE x x2 x2 Hx2in (x = x2 ) ) to the current goal.
Assume Hxx2 .
An exact proof term for the current goal is Hxx2 .
Assume Hxx2 .
An exact proof term for the current goal is Hxx2 .
We prove the intermediate
claim HxX :
x ∈ X .
rewrite the current goal using Hx_eq_x1 (from left to right).
An exact proof term for the current goal is Hx1X .
We use
{ x , x } to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(ReplI X (λx0 : set ⇒ { x0 , x0 } ) x HxX ) .
Apply andI to the current goal.
We will
prove { x , x } ⊆ b1 ∩ b2 .
Let y be given.
Assume Hy .
Apply (UPairE y x x Hy (y ∈ b1 ∩ b2 ) ) to the current goal.
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Hx2 .
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Hx2 .
∎
Proof: Let X be given.
Let U be given.
Assume HUgen .
An
exact proof term for the current goal is
(SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ singleton_basis X , x0 ∈ b ∧ b ⊆ U0 ) U HUgen ) .
Let U be given.
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U HUinPow ) .
Let x be given.
Assume HxU .
We use
{ x , x } to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(ReplI X (λx0 : set ⇒ { x0 , x0 } ) x (HUsubX x HxU ) ) .
Apply andI to the current goal.
An
exact proof term for the current goal is
(UPairI1 x x ) .
Let y be given.
Assume Hy .
Apply (UPairE y x x Hy (y ∈ U ) ) to the current goal.
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxU .
Assume Hyx .
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b ∈ singleton_basis X , x0 ∈ b ∧ b ⊆ U0 ) U HUinPow HUprop ) .
∎
Definition. We define
R to be
real of type
set .
Definition. We define
Q to be
{ q ∈ R | ∃p n : set , p ∈ ω ∧ n ∈ ω ∧ q ∈ R } of type
set .
Definition. We define
Rlt to be
λa b ⇒ a ∈ R ∧ b ∈ R ∧ a < b of type
set → set → prop .
Definition. We define
distance_R2 to be
λp c ⇒ Eps_i (λr ⇒ r ∈ R ) of type
set → set → set .
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, B and B' be given.
Assume HBasis Href .
Let U be given.
Assume HU .
We prove the intermediate
claim HUsubX :
U ⊆ X .
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B , x0 ∈ b0 ∧ b0 ⊆ U0 ) U HU ) ) .
We prove the intermediate
claim HUprop :
∀x ∈ U , ∃b' ∈ B' , x ∈ b' ∧ b' ⊆ U .
An exact proof term for the current goal is (Hprop U HU ) .
An
exact proof term for the current goal is
(SepI (𝒫 X ) (λU0 : set ⇒ ∀x0 ∈ U0 , ∃b0 ∈ B' , x0 ∈ b0 ∧ b0 ⊆ U0 ) U (PowerI X U HUsubX ) HUprop ) .
∎
Definition. We define
subbasis_on to be
λX S ⇒ S ⊆ 𝒫 X of type
set → set → prop .
Proof: Let X and S be given.
Assume HS .
The rest of this subproof is missing.
∎
Proof: Let X and S be given.
Assume HS .
The rest of this subproof is missing.
∎
Proof: Let X, S and T be given.
Assume HS HT HST .
The rest of this subproof is missing.
∎
Proof: Let X, T and A be given.
Assume HT Hlocal .
The rest of this subproof is missing.
∎
Definition. We define
a_elt to be
Empty of type
set .
Proof:
The rest of this subproof is missing.
∎
Proof: Let Fam be given.
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
(SepE1 (⋃ Fam ) (λx0 ⇒ ∀U : set , U ∈ Fam → x0 ∈ U ) x Hx ) .
∎
Proof: Let Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X and U be given.
Assume Hcount .
An exact proof term for the current goal is Hcount .
Assume HUeq .
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnemp HUeq ) .
An
exact proof term for the current goal is
(Hprop (countable (X ∖ U ) ) Hcount_branch Hempty_branch ) .
∎
Proof: Let X and UFam be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X and Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X and Fam be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and A be given.
The rest of this subproof is missing.
∎
Definition. We define
inv_nat to be
λn ⇒ n of type
set → set .
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Definition. We define
Zplus to be
ω of type
set .
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty, Bx and By be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Definition. We define
function_on to be
λf X Y ⇒ ∀x : set , x ∈ X → apply_fun f x ∈ Y of type
set → set → set → prop .
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
An
exact proof term for the current goal is
(SepE1 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HU ) .
We prove the intermediate
claim HEmptyTx :
Empty ∈ Tx .
We prove the intermediate
claim HPred :
∃V ∈ Tx , Empty = V ∩ Y .
We use
Empty to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HEmptyTx .
rewrite the current goal using H1 (from left to right).
Use reflexivity.
We prove the intermediate
claim HXTx :
X ∈ Tx .
An
exact proof term for the current goal is
(topology_has_X X Tx HTx ) .
We prove the intermediate
claim HPredY :
∃V ∈ Tx , Y = V ∩ Y .
We use X to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HXTx .
Let y be given.
An exact proof term for the current goal is (HY y Hy ) .
An exact proof term for the current goal is Hy .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) Y (Self_In_Power Y ) HPredY ) .
Let UFam be given.
Set VFam to be the term
{ V ∈ Tx | ∃U ∈ UFam , U = V ∩ Y } .
We prove the intermediate
claim HVFamTx :
VFam ⊆ Tx .
Let V be given.
An
exact proof term for the current goal is
(SepE1 Tx (λV0 ⇒ ∃U ∈ UFam , U = V0 ∩ Y ) V HV ) .
We prove the intermediate
claim HVFamPower :
VFam ∈ 𝒫 Tx .
Apply PowerI to the current goal.
An exact proof term for the current goal is HVFamTx .
We prove the intermediate
claim HUnionVFam :
⋃ VFam ∈ Tx .
We prove the intermediate
claim HUnionEq :
⋃ UFam = (⋃ VFam ) ∩ Y .
Let x be given.
Let U be given.
An exact proof term for the current goal is (HUFamsub U HUinFam ) .
We prove the intermediate
claim HUexists :
∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSubspace ) .
Apply HUexists to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
We will
prove x ∈ ⋃ VFam .
We prove the intermediate
claim HxV :
x ∈ V .
We prove the intermediate
claim HxVY :
x ∈ V ∩ Y .
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(binintersectE1 V Y x HxVY ) .
We prove the intermediate
claim HVinVFam :
V ∈ VFam .
Apply (SepI Tx (λV0 ⇒ ∃U ∈ UFam , U = V0 ∩ Y ) V HVTx ) to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinFam .
An exact proof term for the current goal is HUeq .
An
exact proof term for the current goal is
(UnionI VFam x V HxV HVinVFam ) .
We prove the intermediate
claim HxVY :
x ∈ V ∩ Y .
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU .
An
exact proof term for the current goal is
(binintersectE2 V Y x HxVY ) .
Let x be given.
We prove the intermediate
claim HxUnionV :
x ∈ ⋃ VFam .
An
exact proof term for the current goal is
(binintersectE1 (⋃ VFam ) Y x Hx ) .
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 (⋃ VFam ) Y x Hx ) .
Let V be given.
We prove the intermediate
claim HVexists :
∃U ∈ UFam , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 Tx (λV0 ⇒ ∃U ∈ UFam , U = V0 ∩ Y ) V HVinVFam ) .
Apply HVexists to the current goal.
Let U be given.
Assume HUandEq .
Apply HUandEq to the current goal.
We prove the intermediate
claim HxU :
x ∈ U .
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HxV .
An exact proof term for the current goal is HxY .
An
exact proof term for the current goal is
(UnionI UFam x U HxU HUinFam ) .
We prove the intermediate
claim HPredUnion :
∃V ∈ Tx , ⋃ UFam = V ∩ Y .
We use
(⋃ VFam ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUnionVFam .
An exact proof term for the current goal is HUnionEq .
We prove the intermediate
claim HUnionInPowerY :
⋃ UFam ∈ 𝒫 Y .
Apply PowerI to the current goal.
Let x be given.
We prove the intermediate
claim HxVY :
x ∈ (⋃ VFam ) ∩ Y .
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is Hx .
An
exact proof term for the current goal is
(binintersectE2 (⋃ VFam ) Y x HxVY ) .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) (⋃ UFam ) HUnionInPowerY HPredUnion ) .
Let U be given.
Let V be given.
We prove the intermediate
claim HUexists :
∃V1 ∈ Tx , U = V1 ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HU ) .
We prove the intermediate
claim HVexists :
∃V2 ∈ Tx , V = V2 ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λV0 : set ⇒ ∃V ∈ Tx , V0 = V ∩ Y ) V HV ) .
Apply HUexists to the current goal.
Let V1 be given.
Assume HV1andEq .
Apply HV1andEq to the current goal.
Apply HVexists to the current goal.
Let V2 be given.
Assume HV2andEq .
Apply HV2andEq to the current goal.
We prove the intermediate
claim HV1V2 :
V1 ∩ V2 ∈ Tx .
We prove the intermediate
claim HIntEq :
U ∩ V = (V1 ∩ V2 ) ∩ Y .
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using HVeq (from left to right).
We will
prove (V1 ∩ Y ) ∩ (V2 ∩ Y ) = (V1 ∩ V2 ) ∩ Y .
Let x be given.
We prove the intermediate
claim HxV1Y :
x ∈ V1 ∩ Y .
An
exact proof term for the current goal is
(binintersectE1 (V1 ∩ Y ) (V2 ∩ Y ) x Hx ) .
We prove the intermediate
claim HxV2Y :
x ∈ V2 ∩ Y .
An
exact proof term for the current goal is
(binintersectE2 (V1 ∩ Y ) (V2 ∩ Y ) x Hx ) .
We prove the intermediate
claim HxV1 :
x ∈ V1 .
An
exact proof term for the current goal is
(binintersectE1 V1 Y x HxV1Y ) .
We prove the intermediate
claim HxV2 :
x ∈ V2 .
An
exact proof term for the current goal is
(binintersectE1 V2 Y x HxV2Y ) .
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 V1 Y x HxV1Y ) .
An exact proof term for the current goal is HxV1 .
An exact proof term for the current goal is HxV2 .
An exact proof term for the current goal is HxY .
Let x be given.
We prove the intermediate
claim HxV1V2 :
x ∈ V1 ∩ V2 .
An
exact proof term for the current goal is
(binintersectE1 (V1 ∩ V2 ) Y x Hx ) .
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 (V1 ∩ V2 ) Y x Hx ) .
We prove the intermediate
claim HxV1 :
x ∈ V1 .
An
exact proof term for the current goal is
(binintersectE1 V1 V2 x HxV1V2 ) .
We prove the intermediate
claim HxV2 :
x ∈ V2 .
An
exact proof term for the current goal is
(binintersectE2 V1 V2 x HxV1V2 ) .
An exact proof term for the current goal is HxV1 .
An exact proof term for the current goal is HxY .
An exact proof term for the current goal is HxV2 .
An exact proof term for the current goal is HxY .
We prove the intermediate
claim HPredInt :
∃W ∈ Tx , U ∩ V = W ∩ Y .
We use
(V1 ∩ V2 ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV1V2 .
An exact proof term for the current goal is HIntEq .
We prove the intermediate
claim HIntInPowerY :
U ∩ V ∈ 𝒫 Y .
Apply PowerI to the current goal.
Let x be given.
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U V x Hx ) .
We prove the intermediate
claim HUinPowerY :
U ∈ 𝒫 Y .
An
exact proof term for the current goal is
(SepE1 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HU ) .
We prove the intermediate
claim HUsub :
U ⊆ Y .
An
exact proof term for the current goal is
(PowerE Y U HUinPowerY ) .
An exact proof term for the current goal is (HUsub x HxU ) .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) (U ∩ V ) HIntInPowerY HPredInt ) .
∎
Proof: Let X, Tx, Y and U be given.
Apply iffI to the current goal.
We will
prove ∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSubspace ) .
Apply andI to the current goal.
We prove the intermediate
claim HUinPowerY :
U ∈ 𝒫 Y .
Apply PowerI to the current goal.
An exact proof term for the current goal is HU .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinPowerY Hexists ) .
∎
Proof: Let X, Tx, Y and B be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and U be given.
We prove the intermediate
claim HYsub :
Y ⊆ X .
We prove the intermediate
claim Hexists :
∃V ∈ Tx , U = V ∩ Y .
Apply Hexists to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
We prove the intermediate
claim HVY :
V ∩ Y ∈ Tx .
We prove the intermediate
claim HUinTx :
U ∈ Tx .
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HVY .
An exact proof term for the current goal is HUinTx .
∎
Proof: Let X, Tx, Y, Ty, A and B be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Y be given.
The rest of this subproof is missing.
∎
Proof: Let W, Y and A be given.
Let x be given.
We prove the intermediate
claim Hpair :
x ∈ W ∩ Y ∧ x ∈ A .
An
exact proof term for the current goal is
(binintersectE (W ∩ Y ) A x Hx ) .
We prove the intermediate
claim HWY :
x ∈ W ∩ Y .
An
exact proof term for the current goal is
(andEL (x ∈ W ∩ Y ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HA :
x ∈ A .
An
exact proof term for the current goal is
(andER (x ∈ W ∩ Y ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HWYpair :
x ∈ W ∧ x ∈ Y .
An
exact proof term for the current goal is
(binintersectE W Y x HWY ) .
We prove the intermediate
claim HW :
x ∈ W .
An
exact proof term for the current goal is
(andEL (x ∈ W ) (x ∈ Y ) HWYpair ) .
An exact proof term for the current goal is HW .
An exact proof term for the current goal is HA .
Let x be given.
We prove the intermediate
claim Hpair :
x ∈ W ∧ x ∈ A .
An
exact proof term for the current goal is
(binintersectE W A x Hx ) .
We prove the intermediate
claim HW :
x ∈ W .
An
exact proof term for the current goal is
(andEL (x ∈ W ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HA :
x ∈ A .
An
exact proof term for the current goal is
(andER (x ∈ W ) (x ∈ A ) Hpair ) .
We prove the intermediate
claim HY :
x ∈ Y .
An exact proof term for the current goal is (Hsub x HA ) .
We prove the intermediate
claim HWY :
x ∈ W ∩ Y .
An
exact proof term for the current goal is
(binintersectI W Y x HW HY ) .
An exact proof term for the current goal is HWY .
An exact proof term for the current goal is HA .
∎
Proof: Let X, Tx, Y and A be given.
Let W be given.
We prove the intermediate
claim HWPowerA :
W ∈ 𝒫 A .
Apply HWexists to the current goal.
Let U be given.
We prove the intermediate
claim HWeqUA :
W = U ∩ A .
We prove the intermediate
claim HUPowerY :
U ∈ 𝒫 Y .
An
exact proof term for the current goal is
(SepE1 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSubY ) .
We prove the intermediate
claim HUexists :
∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSubY ) .
Apply HUexists to the current goal.
Let V be given.
We prove the intermediate
claim HVinTx :
V ∈ Tx .
An
exact proof term for the current goal is
(andEL (V ∈ Tx ) (U = V ∩ Y ) HV ) .
We prove the intermediate
claim HUeqVY :
U = V ∩ Y .
An
exact proof term for the current goal is
(andER (V ∈ Tx ) (U = V ∩ Y ) HV ) .
We prove the intermediate
claim HWeqVA :
W = V ∩ A .
rewrite the current goal using HWeqUA (from left to right).
rewrite the current goal using HUeqVY (from left to right).
We prove the intermediate
claim HWPred :
∃V0 ∈ Tx , W = V0 ∩ A .
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVinTx .
An exact proof term for the current goal is HWeqVA .
An
exact proof term for the current goal is
(SepI (𝒫 A ) (λW0 : set ⇒ ∃V0 ∈ Tx , W0 = V0 ∩ A ) W HWPowerA HWPred ) .
Let W be given.
We prove the intermediate
claim HWPowerA :
W ∈ 𝒫 A .
An
exact proof term for the current goal is
(SepE1 (𝒫 A ) (λW0 : set ⇒ ∃V ∈ Tx , W0 = V ∩ A ) W HW ) .
We prove the intermediate
claim HWexists :
∃V ∈ Tx , W = V ∩ A .
An
exact proof term for the current goal is
(SepE2 (𝒫 A ) (λW0 : set ⇒ ∃V ∈ Tx , W0 = V ∩ A ) W HW ) .
Apply HWexists to the current goal.
Let V be given.
We prove the intermediate
claim HVinTx :
V ∈ Tx .
An
exact proof term for the current goal is
(andEL (V ∈ Tx ) (W = V ∩ A ) HV ) .
We prove the intermediate
claim HWeqVA :
W = V ∩ A .
An
exact proof term for the current goal is
(andER (V ∈ Tx ) (W = V ∩ A ) HV ) .
Set U to be the term
V ∩ Y .
We prove the intermediate
claim HUPowerY :
U ∈ 𝒫 Y .
We prove the intermediate
claim HUPred :
∃V0 ∈ Tx , U = V0 ∩ Y .
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVinTx .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃V0 ∈ Tx , U0 = V0 ∩ Y ) U HUPowerY HUPred ) .
We prove the intermediate
claim HWeqUA :
W = U ∩ A .
rewrite the current goal using HWeqVA (from left to right).
Use symmetry.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinSubY .
An exact proof term for the current goal is HWeqUA .
An
exact proof term for the current goal is
(SepI (𝒫 A ) (λW0 : set ⇒ ∃U0 ∈ subspace_topology X Tx Y , W0 = U0 ∩ A ) W HWPowerA HWPred ) .
∎
Proof: Let X, T, T' and Y be given.
Let W be given.
We prove the intermediate
claim HWPowerY :
W ∈ 𝒫 Y .
An
exact proof term for the current goal is
(SepE1 (𝒫 Y ) (λW0 : set ⇒ ∃V ∈ T' , W0 = V ∩ Y ) W HW ) .
We prove the intermediate
claim HWexists :
∃V ∈ T' , W = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λW0 : set ⇒ ∃V ∈ T' , W0 = V ∩ Y ) W HW ) .
Apply HWexists to the current goal.
Let V' be given.
We prove the intermediate
claim HV'inT' :
V' ∈ T' .
An
exact proof term for the current goal is
(andEL (V' ∈ T' ) (W = V' ∩ Y ) HV' ) .
We prove the intermediate
claim HWeqV'Y :
W = V' ∩ Y .
An
exact proof term for the current goal is
(andER (V' ∈ T' ) (W = V' ∩ Y ) HV' ) .
We prove the intermediate
claim HV'inT :
V' ∈ T .
An exact proof term for the current goal is (Hfiner V' HV'inT' ) .
We prove the intermediate
claim HWPred :
∃V ∈ T , W = V ∩ Y .
We use V' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV'inT .
An exact proof term for the current goal is HWeqV'Y .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λW0 : set ⇒ ∃V ∈ T , W0 = V ∩ Y ) W HWPowerY HWPred ) .
∎
Proof: Let X, Tx and Y be given.
Let U be given.
We prove the intermediate
claim HUPowerY :
U ∈ 𝒫 Y .
An
exact proof term for the current goal is
(SepE1 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSub ) .
We prove the intermediate
claim HUexists :
∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUinSub ) .
Apply HUexists to the current goal.
Let V be given.
We prove the intermediate
claim HVinTx :
V ∈ Tx .
An
exact proof term for the current goal is
(andEL (V ∈ Tx ) (U = V ∩ Y ) HV ) .
We prove the intermediate
claim HUeqVY :
U = V ∩ Y .
An
exact proof term for the current goal is
(andER (V ∈ Tx ) (U = V ∩ Y ) HV ) .
We prove the intermediate
claim HVopen :
open_in X Tx V .
An
exact proof term for the current goal is
(andI (topology_on X Tx ) (V ∈ Tx ) Htop HVinTx ) .
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVopen .
An exact proof term for the current goal is HUeqVY .
∎
Proof: Let X, Tx, Y and Ty be given.
Let U be given.
The rest of this subproof is missing.
∎
Proof: Let X, T, T', Y, U and U' be given.
The rest of this subproof is missing.
∎
Proof: Let X, T, T', Y, U and U' be given.
We will
prove T ⊆ T' ∧ U ⊆ U' .
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let A be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Definition. We define
interior_of to be
λX T A ⇒ { x ∈ X | ∃U : set , U ∈ T ∧ x ∈ U ∧ U ⊆ A } of type
set → set → set → set .
Definition. We define
closure_of to be
λX T A ⇒ { x ∈ X | ∀U : set , U ∈ T → x ∈ U → U ∩ A ≠ Empty } of type
set → set → set → set .
Proof: Let X, Tx and A be given.
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HA x Hx ) .
We prove the intermediate
claim Hcond :
∀U : set , U ∈ Tx → x ∈ U → U ∩ A ≠ Empty .
Let U be given.
We prove the intermediate
claim HxUA :
x ∈ U ∩ A .
An
exact proof term for the current goal is
(binintersectI U A x HxU Hx ) .
We prove the intermediate
claim HxEmpty :
x ∈ Empty .
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HxUA .
An
exact proof term for the current goal is
(EmptyE x HxEmpty ) .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x HxX Hcond ) .
∎
Proof: Let X, Tx, A and B be given.
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(SepE1 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x Hx ) .
We prove the intermediate
claim HcondA :
∀U : set , U ∈ Tx → x ∈ U → U ∩ A ≠ Empty .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x Hx ) .
We prove the intermediate
claim HcondB :
∀U : set , U ∈ Tx → x ∈ U → U ∩ B ≠ Empty .
Let U be given.
We prove the intermediate
claim HUA_ne :
U ∩ A ≠ Empty .
An exact proof term for the current goal is (HcondA U HU HxU ) .
We prove the intermediate
claim HUA_sub_UB :
U ∩ A ⊆ U ∩ B .
Let y be given.
We prove the intermediate
claim HyU :
y ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U A y Hy ) .
We prove the intermediate
claim HyA :
y ∈ A .
An
exact proof term for the current goal is
(binintersectE2 U A y Hy ) .
We prove the intermediate
claim HyB :
y ∈ B .
An exact proof term for the current goal is (HAB y HyA ) .
An
exact proof term for the current goal is
(binintersectI U B y HyU HyB ) .
We prove the intermediate
claim HUA_empty :
U ∩ A = Empty .
We prove the intermediate
claim HUB_sub_Empty :
U ∩ B ⊆ Empty .
rewrite the current goal using Hempty (from left to right).
An
exact proof term for the current goal is
(Subq_tra (U ∩ A ) (U ∩ B ) Empty HUA_sub_UB HUB_sub_Empty ) .
An exact proof term for the current goal is (HUA_ne HUA_empty ) .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ B ≠ Empty ) x HxX HcondB ) .
∎
Proof: Let X, Tx and A be given.
Let x be given.
We prove the intermediate
claim Hexists :
∃U : set , U ∈ Tx ∧ x ∈ U ∧ U ⊆ A .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∃U : set , U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A ) x Hx ) .
Apply Hexists to the current goal.
Let U be given.
We prove the intermediate
claim HU_and_x :
U ∈ Tx ∧ x ∈ U .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HUsub :
U ⊆ A .
An
exact proof term for the current goal is
(andER (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(andER (U ∈ Tx ) (x ∈ U ) HU_and_x ) .
An exact proof term for the current goal is (HUsub x HxU ) .
∎
Proof: Let X, Tx, A and B be given.
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(SepE1 X (λx0 ⇒ ∃U : set , U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A ) x Hx ) .
We prove the intermediate
claim Hexists :
∃U : set , U ∈ Tx ∧ x ∈ U ∧ U ⊆ A .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∃U : set , U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A ) x Hx ) .
Apply Hexists to the current goal.
Let U be given.
We prove the intermediate
claim HU_and_x :
U ∈ Tx ∧ x ∈ U .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HUsub_A :
U ⊆ A .
An
exact proof term for the current goal is
(andER (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HU :
U ∈ Tx .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ) (x ∈ U ) HU_and_x ) .
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(andER (U ∈ Tx ) (x ∈ U ) HU_and_x ) .
We prove the intermediate
claim HUsub_B :
U ⊆ B .
An
exact proof term for the current goal is
(Subq_tra U A B HUsub_A HAB ) .
We prove the intermediate
claim Hwitness :
U ∈ Tx ∧ x ∈ U ∧ U ⊆ B .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU .
An exact proof term for the current goal is HxU .
An exact proof term for the current goal is HUsub_B .
We prove the intermediate
claim Hexists_B :
∃V : set , V ∈ Tx ∧ x ∈ V ∧ V ⊆ B .
We use U to witness the existential quantifier.
An exact proof term for the current goal is Hwitness .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∃V : set , V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ B ) x HxX Hexists_B ) .
∎
Proof: Let X, Tx and U be given.
Let x be given.
We prove the intermediate
claim HUsub :
U ⊆ X .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HUsub x Hx ) .
We prove the intermediate
claim Hwitness :
U ∈ Tx ∧ x ∈ U ∧ U ⊆ U .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU .
An exact proof term for the current goal is Hx .
An
exact proof term for the current goal is
(Subq_ref U ) .
We prove the intermediate
claim Hexists :
∃V : set , V ∈ Tx ∧ x ∈ V ∧ V ⊆ U .
We use U to witness the existential quantifier.
An exact proof term for the current goal is Hwitness .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∃V : set , V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ U ) x HxX Hexists ) .
∎
Proof: Let X and Tx be given.
∎
Proof: Let X and Tx be given.
We prove the intermediate
claim HXopen :
X ∈ Tx .
An
exact proof term for the current goal is
(topology_has_X X Tx Htop ) .
An
exact proof term for the current goal is
(open_interior_eq X Tx X Htop HXopen ) .
∎
Proof: Let X, Tx and A be given.
Set F to be the term
{ U ∈ Tx | U ⊆ A } .
We prove the intermediate
claim Hint_eq_union :
interior_of X Tx A = ⋃ F .
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(SepE1 X (λx0 ⇒ ∃U : set , U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A ) x Hx ) .
We prove the intermediate
claim Hexists :
∃U : set , U ∈ Tx ∧ x ∈ U ∧ U ⊆ A .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∃U : set , U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A ) x Hx ) .
Apply Hexists to the current goal.
Let U be given.
We prove the intermediate
claim HU_and_x :
U ∈ Tx ∧ x ∈ U .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HUsub :
U ⊆ A .
An
exact proof term for the current goal is
(andER (U ∈ Tx ∧ x ∈ U ) (U ⊆ A ) HU_conj ) .
We prove the intermediate
claim HU :
U ∈ Tx .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ) (x ∈ U ) HU_and_x ) .
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(andER (U ∈ Tx ) (x ∈ U ) HU_and_x ) .
We prove the intermediate
claim HUinF :
U ∈ F .
Apply SepI to the current goal.
An exact proof term for the current goal is HU .
An exact proof term for the current goal is HUsub .
An
exact proof term for the current goal is
(UnionI F x U HxU HUinF ) .
Let x be given.
Let U be given.
We prove the intermediate
claim HU :
U ∈ Tx .
An
exact proof term for the current goal is
(SepE1 Tx (λU0 ⇒ U0 ⊆ A ) U HUinF ) .
We prove the intermediate
claim HUsub :
U ⊆ A .
An
exact proof term for the current goal is
(SepE2 Tx (λU0 ⇒ U0 ⊆ A ) U HUinF ) .
We prove the intermediate
claim HUsub_X :
U ⊆ X .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HUsub_X x HxU ) .
We prove the intermediate
claim Hwitness :
U ∈ Tx ∧ x ∈ U ∧ U ⊆ A .
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU .
An exact proof term for the current goal is HxU .
An exact proof term for the current goal is HUsub .
We prove the intermediate
claim Hexists :
∃V : set , V ∈ Tx ∧ x ∈ V ∧ V ⊆ A .
We use U to witness the existential quantifier.
An exact proof term for the current goal is Hwitness .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∃V : set , V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ A ) x HxX Hexists ) .
We prove the intermediate
claim HF_sub_Tx :
F ⊆ Tx .
Let U be given.
An
exact proof term for the current goal is
(SepE1 Tx (λU0 ⇒ U0 ⊆ A ) U HU ) .
We prove the intermediate
claim Hunion_in_Tx :
⋃ F ∈ Tx .
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
We prove the intermediate
claim HAB_union_A :
A ⊆ A ∪ B .
Let x be given.
An
exact proof term for the current goal is
(binunionI1 A B x Hx ) .
We prove the intermediate
claim HAB_union_B :
B ⊆ A ∪ B .
Let x be given.
An
exact proof term for the current goal is
(binunionI2 A B x Hx ) .
We prove the intermediate
claim HAB_sub :
A ∪ B ⊆ X .
Let x be given.
Apply (binunionE A B x Hx ) to the current goal.
An exact proof term for the current goal is (HA x HxA ) .
An exact proof term for the current goal is (HB x HxB ) .
An
exact proof term for the current goal is
(interior_monotone X Tx A (A ∪ B ) Htop HAB_union_A ) .
An
exact proof term for the current goal is
(interior_monotone X Tx B (A ∪ B ) Htop HAB_union_B ) .
Let x be given.
An exact proof term for the current goal is (HintA x HxA ) .
An exact proof term for the current goal is (HintB x HxB ) .
∎
Proof: Let X, Tx, A and B be given.
We prove the intermediate
claim HAB_A :
A ∩ B ⊆ A .
We prove the intermediate
claim HAB_B :
A ∩ B ⊆ B .
An
exact proof term for the current goal is
(interior_monotone X Tx (A ∩ B ) A Htop HAB_A ) .
An
exact proof term for the current goal is
(interior_monotone X Tx (A ∩ B ) B Htop HAB_B ) .
Let x be given.
An exact proof term for the current goal is (HintAB_A x Hx ) .
An exact proof term for the current goal is (HintAB_B x Hx ) .
∎
Proof: Let X, Tx and A be given.
We prove the intermediate
claim HintA_open :
interior_of X Tx A ∈ Tx .
∎
Proof: Let X, Tx and A be given.
∎
Proof: Let X, Tx and A be given.
Let x be given.
An
exact proof term for the current goal is
(SepE1 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x Hx ) .
∎
Proof: Let X, Tx, A and B be given.
We prove the intermediate
claim HAB_union :
A ⊆ A ∪ B .
Let x be given.
An
exact proof term for the current goal is
(binunionI1 A B x Hx ) .
We prove the intermediate
claim HBB_union :
B ⊆ A ∪ B .
Let x be given.
An
exact proof term for the current goal is
(binunionI2 A B x Hx ) .
We prove the intermediate
claim HAB_sub :
A ∪ B ⊆ X .
Let x be given.
Apply (binunionE A B x Hx ) to the current goal.
An exact proof term for the current goal is (HA x HxA ) .
An exact proof term for the current goal is (HB x HxB ) .
An
exact proof term for the current goal is
(closure_monotone X Tx A (A ∪ B ) Htop HAB_union HAB_sub ) .
An
exact proof term for the current goal is
(closure_monotone X Tx B (A ∪ B ) Htop HBB_union HAB_sub ) .
Let x be given.
An exact proof term for the current goal is (HclA x HxA ) .
An exact proof term for the current goal is (HclB x HxB ) .
∎
Proof: Let X and Tx be given.
Let x be given.
Apply (SepE X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ Empty ≠ Empty ) x Hx ) to the current goal.
We prove the intermediate
claim HXopen :
X ∈ Tx .
An
exact proof term for the current goal is
(topology_has_X X Tx Htop ) .
An exact proof term for the current goal is (Hcond X HXopen HxX ) .
Apply HXne to the current goal.
An exact proof term for the current goal is HXempty .
∎
Proof: Let X and Tx be given.
∎
Proof: Let X, Tx and A be given.
We prove the intermediate
claim HclA_sub :
closure_of X Tx A ⊆ X .
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
We prove the intermediate
claim HAB_A :
A ∩ B ⊆ A .
We prove the intermediate
claim HAB_B :
A ∩ B ⊆ B .
We prove the intermediate
claim HAB_X :
A ∩ B ⊆ X .
Let x be given.
An
exact proof term for the current goal is
(HA x (binintersectE1 A B x Hx ) ) .
An
exact proof term for the current goal is
(closure_monotone X Tx (A ∩ B ) A Htop HAB_A HA ) .
An
exact proof term for the current goal is
(closure_monotone X Tx (A ∩ B ) B Htop HAB_B HB ) .
Let x be given.
An exact proof term for the current goal is (HclAB_A x Hx ) .
An exact proof term for the current goal is (HclAB_B x Hx ) .
∎
Proof: Let X, Tx and C be given.
We prove the intermediate
claim HCsub_and_ex :
C ⊆ X ∧ ∃U ∈ Tx , C = X ∖ U .
We prove the intermediate
claim HCsub :
C ⊆ X .
An
exact proof term for the current goal is
(andEL (C ⊆ X ) (∃U ∈ Tx , C = X ∖ U ) HCsub_and_ex ) .
The rest of this subproof is missing.
∎
Proof: Let X and T be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and A be given.
Apply iffI to the current goal.
An exact proof term for the current goal is HAclosed .
Apply HexU to the current goal.
Let U be given.
Assume HandEq .
Apply HandEq to the current goal.
We prove the intermediate
claim HUexV :
∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 : set ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HUsubspace ) .
Apply HUexV to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
Set C to be the term
X ∖ V .
We prove the intermediate
claim HCclosed :
closed_in X Tx C .
Apply andI to the current goal.
An exact proof term for the current goal is HTx .
Apply andI to the current goal.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV .
We prove the intermediate
claim HAeqC :
A = C ∩ Y .
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HUeq (from left to right).
We will
prove Y ∖ (V ∩ Y ) = (X ∖ V ) ∩ Y .
Let x be given.
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(setminusE1 Y (V ∩ Y ) x Hx ) .
We prove the intermediate
claim HxnotVY :
x ∉ V ∩ Y .
An
exact proof term for the current goal is
(setminusE2 Y (V ∩ Y ) x Hx ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
Apply HxnotVY to the current goal.
An exact proof term for the current goal is HxV .
An exact proof term for the current goal is HxY .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HY x HxY ) .
An exact proof term for the current goal is HxX .
An exact proof term for the current goal is HxnotV .
An exact proof term for the current goal is HxY .
Let x be given.
We prove the intermediate
claim HxXV :
x ∈ X ∖ V .
An
exact proof term for the current goal is
(binintersectE1 (X ∖ V ) Y x Hx ) .
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 (X ∖ V ) Y x Hx ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
An
exact proof term for the current goal is
(setminusE2 X V x HxXV ) .
An exact proof term for the current goal is HxY .
Apply HxnotV to the current goal.
An
exact proof term for the current goal is
(binintersectE1 V Y x HxVY ) .
We use C to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HCclosed .
An exact proof term for the current goal is HAeqC .
Apply Hexists to the current goal.
Let C be given.
Assume HCandEq .
Apply HCandEq to the current goal.
We prove the intermediate
claim HCdef :
topology_on X Tx ∧ (C ⊆ X ∧ ∃V ∈ Tx , C = X ∖ V ) .
An exact proof term for the current goal is HCclosed .
We prove the intermediate
claim HCandEx :
C ⊆ X ∧ ∃V ∈ Tx , C = X ∖ V .
An
exact proof term for the current goal is
(andER (topology_on X Tx ) (C ⊆ X ∧ ∃V ∈ Tx , C = X ∖ V ) HCdef ) .
We prove the intermediate
claim HexV :
∃V ∈ Tx , C = X ∖ V .
An
exact proof term for the current goal is
(andER (C ⊆ X ) (∃V ∈ Tx , C = X ∖ V ) HCandEx ) .
Apply HexV to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
Set U to be the term
V ∩ Y .
We prove the intermediate
claim HUinPowerY :
U ∈ 𝒫 Y .
Apply PowerI to the current goal.
We prove the intermediate
claim HPred :
∃W ∈ Tx , U = W ∩ Y .
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV .
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 : set ⇒ ∃W ∈ Tx , U0 = W ∩ Y ) U HUinPowerY HPred ) .
We prove the intermediate
claim HAeqYU :
A = Y ∖ U .
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HCeq (from left to right).
We will
prove (X ∖ V ) ∩ Y = Y ∖ (V ∩ Y ) .
Let x be given.
We prove the intermediate
claim HxXV :
x ∈ X ∖ V .
An
exact proof term for the current goal is
(binintersectE1 (X ∖ V ) Y x Hx ) .
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 (X ∖ V ) Y x Hx ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
An
exact proof term for the current goal is
(setminusE2 X V x HxXV ) .
An exact proof term for the current goal is HxY .
Apply HxnotV to the current goal.
An
exact proof term for the current goal is
(binintersectE1 V Y x HxVY ) .
Let x be given.
We prove the intermediate
claim HxY :
x ∈ Y .
An
exact proof term for the current goal is
(setminusE1 Y (V ∩ Y ) x Hx ) .
We prove the intermediate
claim HxnotVY :
x ∉ V ∩ Y .
An
exact proof term for the current goal is
(setminusE2 Y (V ∩ Y ) x Hx ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
Apply HxnotVY to the current goal.
An exact proof term for the current goal is HxV .
An exact proof term for the current goal is HxY .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HY x HxY ) .
An exact proof term for the current goal is HxX .
An exact proof term for the current goal is HxnotV .
An exact proof term for the current goal is HxY .
We prove the intermediate
claim HAsub :
A ⊆ Y .
rewrite the current goal using HAeq (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is HTsubspace .
Apply andI to the current goal.
An exact proof term for the current goal is HAsub .
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUsubspace .
An exact proof term for the current goal is HAeqYU .
∎
Proof: Let X, Tx, Y and A be given.
We prove the intermediate
claim HYsub :
Y ⊆ X .
We prove the intermediate
claim Hexists :
∃C : set , closed_in X Tx C ∧ A = C ∩ Y .
An exact proof term for the current goal is HA .
Apply Hexists to the current goal.
Let C be given.
We prove the intermediate
claim HCclosed :
closed_in X Tx C .
An
exact proof term for the current goal is
(andEL (closed_in X Tx C ) (A = C ∩ Y ) HCandA ) .
We prove the intermediate
claim HAeq :
A = C ∩ Y .
An
exact proof term for the current goal is
(andER (closed_in X Tx C ) (A = C ∩ Y ) HCandA ) .
We prove the intermediate
claim HCexists :
∃U ∈ Tx , C = X ∖ U .
Apply HCexists to the current goal.
Let U be given.
We prove the intermediate
claim HUinTx :
U ∈ Tx .
An
exact proof term for the current goal is
(andEL (U ∈ Tx ) (C = X ∖ U ) HU ) .
We prove the intermediate
claim HCeq :
C = X ∖ U .
An
exact proof term for the current goal is
(andER (U ∈ Tx ) (C = X ∖ U ) HU ) .
We prove the intermediate
claim HYexists :
∃V ∈ Tx , Y = X ∖ V .
Apply HYexists to the current goal.
Let V be given.
We prove the intermediate
claim HVinTx :
V ∈ Tx .
An
exact proof term for the current goal is
(andEL (V ∈ Tx ) (Y = X ∖ V ) HV ) .
We prove the intermediate
claim HYeq :
Y = X ∖ V .
An
exact proof term for the current goal is
(andER (V ∈ Tx ) (Y = X ∖ V ) HV ) .
We prove the intermediate
claim HAeqSetminus :
A = (X ∖ U ) ∩ (X ∖ V ) .
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HCeq (from left to right).
rewrite the current goal using HYeq (from left to right).
Use reflexivity.
We prove the intermediate
claim HDeM :
(X ∖ U ) ∩ (X ∖ V ) = X ∖ (U ∪ V ) .
Let x be given.
We will
prove x ∈ X ∖ (U ∪ V ) .
We prove the intermediate
claim HxXU :
x ∈ X ∖ U .
An
exact proof term for the current goal is
(binintersectE1 (X ∖ U ) (X ∖ V ) x Hx ) .
We prove the intermediate
claim HxXV :
x ∈ X ∖ V .
An
exact proof term for the current goal is
(binintersectE2 (X ∖ U ) (X ∖ V ) x Hx ) .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X U x HxXU ) .
We prove the intermediate
claim HxninU :
x ∉ U .
An
exact proof term for the current goal is
(setminusE2 X U x HxXU ) .
We prove the intermediate
claim HxninV :
x ∉ V .
An
exact proof term for the current goal is
(setminusE2 X V x HxXV ) .
An exact proof term for the current goal is HxX .
Apply (binunionE U V x HxUV ) to the current goal.
An exact proof term for the current goal is (HxninU HxU ) .
An exact proof term for the current goal is (HxninV HxV ) .
Let x be given.
We will
prove x ∈ (X ∖ U ) ∩ (X ∖ V ) .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (U ∪ V ) x Hx ) .
We prove the intermediate
claim HxninUV :
x ∉ U ∪ V .
An
exact proof term for the current goal is
(setminusE2 X (U ∪ V ) x Hx ) .
An exact proof term for the current goal is HxX .
We prove the intermediate
claim HxUV :
x ∈ U ∪ V .
An
exact proof term for the current goal is
(binunionI1 U V x HxU ) .
An exact proof term for the current goal is (HxninUV HxUV ) .
An exact proof term for the current goal is HxX .
We prove the intermediate
claim HxUV :
x ∈ U ∪ V .
An
exact proof term for the current goal is
(binunionI2 U V x HxV ) .
An exact proof term for the current goal is (HxninUV HxUV ) .
We prove the intermediate
claim HUV :
U ∪ V ∈ Tx .
We prove the intermediate
claim HUV_eq :
U ∪ V = ⋃ (UPair U V ) .
Let x be given.
Apply (binunionE U V x Hx ) to the current goal.
Apply (UnionI (UPair U V ) x U HxU ) to the current goal.
An
exact proof term for the current goal is
(UPairI1 U V ) .
Apply (UnionI (UPair U V ) x V HxV ) to the current goal.
An
exact proof term for the current goal is
(UPairI2 U V ) .
Let x be given.
Let W be given.
Apply (UPairE W U V HWin ) to the current goal.
We prove the intermediate
claim HxU :
x ∈ U .
rewrite the current goal using HWeqU (from right to left).
An exact proof term for the current goal is HxW .
An
exact proof term for the current goal is
(binunionI1 U V x HxU ) .
We prove the intermediate
claim HxV :
x ∈ V .
rewrite the current goal using HWeqV (from right to left).
An exact proof term for the current goal is HxW .
An
exact proof term for the current goal is
(binunionI2 U V x HxV ) .
rewrite the current goal using HUV_eq (from left to right).
We prove the intermediate
claim HUPairSub :
UPair U V ⊆ Tx .
Let W be given.
Apply (UPairE W U V HW ) to the current goal.
rewrite the current goal using HWeqU (from left to right).
An exact proof term for the current goal is HUinTx .
rewrite the current goal using HWeqV (from left to right).
An exact proof term for the current goal is HVinTx .
We prove the intermediate
claim HAeqFinal :
A = X ∖ (U ∪ V ) .
rewrite the current goal using HAeqSetminus (from left to right).
An exact proof term for the current goal is HDeM .
Apply andI to the current goal.
An exact proof term for the current goal is HTx .
Apply andI to the current goal.
rewrite the current goal using HAeqFinal (from left to right).
An
exact proof term for the current goal is
(setminus_Subq X (U ∪ V ) ) .
We will
prove ∃U0 ∈ Tx , A = X ∖ U0 .
We use
(U ∪ V ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUV .
An exact proof term for the current goal is HAeqFinal .
∎
Proof: Let X, Tx, Y and A be given.
Let y be given.
We prove the intermediate
claim HyY :
y ∈ Y .
We prove the intermediate
claim HyX :
y ∈ X .
An exact proof term for the current goal is (HY y HyY ) .
We prove the intermediate
claim HyCond :
∀V : set , V ∈ Tx → y ∈ V → V ∩ A ≠ Empty .
Let V be given.
Set U to be the term
V ∩ Y .
We prove the intermediate
claim HUinPower :
U ∈ 𝒫 Y .
Apply PowerI to the current goal.
We prove the intermediate
claim HPred :
∃W ∈ Tx , U = W ∩ Y .
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV .
Use reflexivity.
An
exact proof term for the current goal is
(SepI (𝒫 Y ) (λU0 ⇒ ∃W ∈ Tx , U0 = W ∩ Y ) U HUinPower HPred ) .
We prove the intermediate
claim HyU :
y ∈ U .
An exact proof term for the current goal is HyV .
An exact proof term for the current goal is HyY .
We prove the intermediate
claim HUA_ne :
U ∩ A ≠ Empty .
An exact proof term for the current goal is (HysubCond U HU HyU ) .
We prove the intermediate
claim HUA_sub_VA :
U ∩ A ⊆ V ∩ A .
Let z be given.
We prove the intermediate
claim HzU :
z ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U A z Hz ) .
We prove the intermediate
claim HzV :
z ∈ V .
An
exact proof term for the current goal is
(binintersectE1 V Y z HzU ) .
We prove the intermediate
claim HzA :
z ∈ A .
An
exact proof term for the current goal is
(binintersectE2 U A z Hz ) .
An
exact proof term for the current goal is
(binintersectI V A z HzV HzA ) .
We prove the intermediate
claim HUA_sub_Empty :
U ∩ A ⊆ Empty .
rewrite the current goal using HVA_empty (from right to left).
An exact proof term for the current goal is HUA_sub_VA .
We prove the intermediate
claim HUA_empty :
U ∩ A = Empty .
An
exact proof term for the current goal is
(Empty_Subq_eq (U ∩ A ) HUA_sub_Empty ) .
An exact proof term for the current goal is (HUA_ne HUA_empty ) .
An
exact proof term for the current goal is
(SepI X (λy0 ⇒ ∀V : set , V ∈ Tx → y0 ∈ V → V ∩ A ≠ Empty ) y HyX HyCond ) .
An exact proof term for the current goal is HyY .
Let y be given.
We prove the intermediate
claim HyClX :
y ∈ closure_of X Tx A .
We prove the intermediate
claim HyY :
y ∈ Y .
We prove the intermediate
claim HyXCond :
∀V : set , V ∈ Tx → y ∈ V → V ∩ A ≠ Empty .
An
exact proof term for the current goal is
(SepE2 X (λy0 ⇒ ∀V : set , V ∈ Tx → y0 ∈ V → V ∩ A ≠ Empty ) y HyClX ) .
Let U be given.
We prove the intermediate
claim HUex :
∃V ∈ Tx , U = V ∩ Y .
An
exact proof term for the current goal is
(SepE2 (𝒫 Y ) (λU0 ⇒ ∃V ∈ Tx , U0 = V ∩ Y ) U HU ) .
Apply HUex to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
We prove the intermediate
claim HyV :
y ∈ V .
We prove the intermediate
claim HyVY :
y ∈ V ∩ Y .
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU .
An
exact proof term for the current goal is
(binintersectE1 V Y y HyVY ) .
We prove the intermediate
claim HVA_ne :
V ∩ A ≠ Empty .
An exact proof term for the current goal is (HyXCond V HV HyV ) .
rewrite the current goal using HUeq (from left to right).
We prove the intermediate
claim HVA_sub_VYA :
V ∩ (Y ∩ A ) ⊆ V ∩ A .
Let z be given.
We prove the intermediate
claim HzV :
z ∈ V .
An
exact proof term for the current goal is
(binintersectE1 V (Y ∩ A ) z Hz ) .
We prove the intermediate
claim HzYA :
z ∈ Y ∩ A .
An
exact proof term for the current goal is
(binintersectE2 V (Y ∩ A ) z Hz ) .
We prove the intermediate
claim HzA :
z ∈ A .
An
exact proof term for the current goal is
(binintersectE2 Y A z HzYA ) .
An
exact proof term for the current goal is
(binintersectI V A z HzV HzA ) .
We prove the intermediate
claim HVYAeq :
V ∩ (Y ∩ A ) = (V ∩ Y ) ∩ A .
Let z be given.
We prove the intermediate
claim HzV :
z ∈ V .
An
exact proof term for the current goal is
(binintersectE1 V (Y ∩ A ) z Hz ) .
We prove the intermediate
claim HzYA :
z ∈ Y ∩ A .
An
exact proof term for the current goal is
(binintersectE2 V (Y ∩ A ) z Hz ) .
We prove the intermediate
claim HzY :
z ∈ Y .
An
exact proof term for the current goal is
(binintersectE1 Y A z HzYA ) .
We prove the intermediate
claim HzA :
z ∈ A .
An
exact proof term for the current goal is
(binintersectE2 Y A z HzYA ) .
We prove the intermediate
claim HzVY :
z ∈ V ∩ Y .
An
exact proof term for the current goal is
(binintersectI V Y z HzV HzY ) .
An
exact proof term for the current goal is
(binintersectI (V ∩ Y ) A z HzVY HzA ) .
Let z be given.
We prove the intermediate
claim HzVY :
z ∈ V ∩ Y .
An
exact proof term for the current goal is
(binintersectE1 (V ∩ Y ) A z Hz ) .
We prove the intermediate
claim HzV :
z ∈ V .
An
exact proof term for the current goal is
(binintersectE1 V Y z HzVY ) .
We prove the intermediate
claim HzY :
z ∈ Y .
An
exact proof term for the current goal is
(binintersectE2 V Y z HzVY ) .
We prove the intermediate
claim HzA :
z ∈ A .
An
exact proof term for the current goal is
(binintersectE2 (V ∩ Y ) A z Hz ) .
We prove the intermediate
claim HzYA :
z ∈ Y ∩ A .
An
exact proof term for the current goal is
(binintersectI Y A z HzY HzA ) .
An
exact proof term for the current goal is
(binintersectI V (Y ∩ A ) z HzV HzYA ) .
We prove the intermediate
claim HVYAempty2 :
V ∩ (Y ∩ A ) = Empty .
rewrite the current goal using HVYAeq (from left to right).
An exact proof term for the current goal is HVYAempty .
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and x be given.
Apply iffI to the current goal.
We will
prove ∀U ∈ Tx , x ∈ U → U ∩ A ≠ Empty .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x Hx ) .
We prove the intermediate
claim HXinTx :
X ∈ Tx .
An
exact proof term for the current goal is
(topology_has_X X Tx HTx ) .
Apply xm (x ∈ X ) to the current goal.
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x HxX Hcond ) .
Apply FalseE to the current goal.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Let F be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and x be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, seq, x and y be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and A be given.
∎
Proof: Let X, Tx, Y, Ty, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, U and A be given.
We prove the intermediate
claim HUtop :
U ∈ Tx .
We prove the intermediate
claim HAdef :
A ⊆ X ∧ (∃V ∈ Tx , A = X ∖ V ) .
An
exact proof term for the current goal is
(andER (topology_on X Tx ) (A ⊆ X ∧ (∃V ∈ Tx , A = X ∖ V ) ) HA ) .
We prove the intermediate
claim HexV :
∃V ∈ Tx , A = X ∖ V .
An
exact proof term for the current goal is
(andER (A ⊆ X ) (∃V ∈ Tx , A = X ∖ V ) HAdef ) .
Apply HexV to the current goal.
Let V be given.
Assume HVandEq .
Apply HVandEq to the current goal.
Apply andI to the current goal.
We prove the intermediate
claim HUsub :
U ⊆ X .
We prove the intermediate
claim HUminusA_eq_UinterV :
U ∖ A = U ∩ V .
rewrite the current goal using HAeq (from left to right).
Let x be given.
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(setminusE1 U (X ∖ V ) x Hx ) .
We prove the intermediate
claim HxnotXV :
x ∉ X ∖ V .
An
exact proof term for the current goal is
(setminusE2 U (X ∖ V ) x Hx ) .
We prove the intermediate
claim HxV :
x ∈ V .
We prove the intermediate
claim HxX :
x ∈ X .
An exact proof term for the current goal is (HUsub x HxU ) .
Apply xm (x ∈ V ) to the current goal.
Assume Hv .
An exact proof term for the current goal is Hv .
Assume Hnv .
Apply FalseE to the current goal.
Apply HxnotXV to the current goal.
An
exact proof term for the current goal is
(setminusI X V x HxX Hnv ) .
An
exact proof term for the current goal is
(binintersectI U V x HxU HxV ) .
Let x be given.
We prove the intermediate
claim HxU :
x ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U V x Hx ) .
We prove the intermediate
claim HxV :
x ∈ V .
An
exact proof term for the current goal is
(binintersectE2 U V x Hx ) .
We prove the intermediate
claim HxnotXV :
x ∉ X ∖ V .
Assume H .
An exact proof term for the current goal is HxV .
An
exact proof term for the current goal is
(setminusI U (X ∖ V ) x HxU HxnotXV ) .
rewrite the current goal using HUminusA_eq_UinterV (from left to right).
We prove the intermediate
claim HUinterV :
U ∩ V ∈ Tx .
An
exact proof term for the current goal is
(andI (topology_on X Tx ) (U ∩ V ∈ Tx ) Htop HUinterV ) .
We prove the intermediate
claim HAsub :
A ⊆ X .
An
exact proof term for the current goal is
(andEL (A ⊆ X ) (∃V0 ∈ Tx , A = X ∖ V0 ) HAdef ) .
We prove the intermediate
claim HAminusU_sub :
A ∖ U ⊆ X .
Let x be given.
Assume Hx .
We prove the intermediate
claim HxA :
x ∈ A .
An
exact proof term for the current goal is
(setminusE1 A U x Hx ) .
An exact proof term for the current goal is (HAsub x HxA ) .
We prove the intermediate
claim HVU :
V ∪ U ∈ Tx .
Set UFam to be the term
UPair V U .
We prove the intermediate
claim HUFamsub :
UFam ⊆ Tx .
Let W be given.
Apply (UPairE W V U HW ) to the current goal.
Assume HWeqV .
rewrite the current goal using HWeqV (from left to right).
An exact proof term for the current goal is HV .
Assume HWeqU .
rewrite the current goal using HWeqU (from left to right).
An exact proof term for the current goal is HUtop .
We prove the intermediate
claim HUnionVU :
⋃ UFam = V ∪ U .
Let x be given.
Let W be given.
Apply (UPairE W V U HW ) to the current goal.
Assume HWeqV .
We prove the intermediate
claim HxV :
x ∈ V .
rewrite the current goal using HWeqV (from right to left).
An exact proof term for the current goal is HxW .
An
exact proof term for the current goal is
(binunionI1 V U x HxV ) .
Assume HWeqU .
We prove the intermediate
claim HxU :
x ∈ U .
rewrite the current goal using HWeqU (from right to left).
An exact proof term for the current goal is HxW .
An
exact proof term for the current goal is
(binunionI2 V U x HxU ) .
Let x be given.
Apply (binunionE V U x Hx ) to the current goal.
Assume HxV .
An
exact proof term for the current goal is
(UnionI UFam x V HxV (UPairI1 V U ) ) .
Assume HxU .
An
exact proof term for the current goal is
(UnionI UFam x U HxU (UPairI2 V U ) ) .
rewrite the current goal using HUnionVU (from right to left).
We prove the intermediate
claim HAminusU_eq_XminusVU :
A ∖ U = X ∖ (V ∪ U ) .
rewrite the current goal using HAeq (from left to right).
Let x be given.
We prove the intermediate
claim HxXV :
x ∈ X ∖ V .
An
exact proof term for the current goal is
(setminusE1 (X ∖ V ) U x Hx ) .
We prove the intermediate
claim HxnotU :
x ∉ U .
An
exact proof term for the current goal is
(setminusE2 (X ∖ V ) U x Hx ) .
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X V x HxXV ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
An
exact proof term for the current goal is
(setminusE2 X V x HxXV ) .
We prove the intermediate
claim HxnotVU :
x ∉ V ∪ U .
Assume H .
Apply (binunionE V U x H ) to the current goal.
Assume HxV .
An exact proof term for the current goal is (HxnotV HxV ) .
Assume HxU .
An exact proof term for the current goal is (HxnotU HxU ) .
An
exact proof term for the current goal is
(setminusI X (V ∪ U ) x HxX HxnotVU ) .
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(setminusE1 X (V ∪ U ) x Hx ) .
We prove the intermediate
claim HxnotVU :
x ∉ V ∪ U .
An
exact proof term for the current goal is
(setminusE2 X (V ∪ U ) x Hx ) .
We prove the intermediate
claim HxnotV :
x ∉ V .
Assume HxV .
Apply HxnotVU to the current goal.
An
exact proof term for the current goal is
(binunionI1 V U x HxV ) .
We prove the intermediate
claim HxnotU :
x ∉ U .
Assume HxU .
Apply HxnotVU to the current goal.
An
exact proof term for the current goal is
(binunionI2 V U x HxU ) .
We prove the intermediate
claim HxXV :
x ∈ X ∖ V .
An
exact proof term for the current goal is
(setminusI X V x HxX HxnotV ) .
An
exact proof term for the current goal is
(setminusI (X ∖ V ) U x HxXV HxnotU ) .
We prove the intermediate
claim HPred :
∃W ∈ Tx , A ∖ U = X ∖ W .
We use
(V ∪ U ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVU .
An exact proof term for the current goal is HAminusU_eq_XminusVU .
An
exact proof term for the current goal is
(andI (topology_on X Tx ) (A ∖ U ⊆ X ∧ (∃W ∈ Tx , A ∖ U = X ∖ W ) ) Htop (andI (A ∖ U ⊆ X ) (∃W ∈ Tx , A ∖ U = X ∖ W ) HAminusU_sub HPred ) ) .
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
Apply andI to the current goal.
The rest of this subproof is missing.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
Let x be given.
We prove the intermediate
claim HxX :
x ∈ X .
An
exact proof term for the current goal is
(SepE1 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ (A ∩ B ) ≠ Empty ) x Hx ) .
We prove the intermediate
claim HxAB :
∀U : set , U ∈ Tx → x ∈ U → U ∩ (A ∩ B ) ≠ Empty .
An
exact proof term for the current goal is
(SepE2 X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ (A ∩ B ) ≠ Empty ) x Hx ) .
We prove the intermediate
claim HxA :
x ∈ X ∧ (∀U : set , U ∈ Tx → x ∈ U → U ∩ A ≠ Empty ) .
Apply andI to the current goal.
An exact proof term for the current goal is HxX .
Let U be given.
We prove the intermediate
claim HABne :
U ∩ (A ∩ B ) ≠ Empty .
An exact proof term for the current goal is (HxAB U HU HxU ) .
Apply HABne to the current goal.
Let y be given.
We prove the intermediate
claim HyU :
y ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U (A ∩ B ) y Hy ) .
We prove the intermediate
claim HyAB :
y ∈ A ∩ B .
An
exact proof term for the current goal is
(binintersectE2 U (A ∩ B ) y Hy ) .
We prove the intermediate
claim HyA :
y ∈ A .
An
exact proof term for the current goal is
(binintersectE1 A B y HyAB ) .
We prove the intermediate
claim HyUA :
y ∈ U ∩ A .
An exact proof term for the current goal is HyU .
An exact proof term for the current goal is HyA .
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUA .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty ) x HxX (andER (x ∈ X ) (∀U : set , U ∈ Tx → x ∈ U → U ∩ A ≠ Empty ) HxA ) ) .
We prove the intermediate
claim HxB :
x ∈ X ∧ (∀U : set , U ∈ Tx → x ∈ U → U ∩ B ≠ Empty ) .
Apply andI to the current goal.
An exact proof term for the current goal is HxX .
Let U be given.
We prove the intermediate
claim HABne :
U ∩ (A ∩ B ) ≠ Empty .
An exact proof term for the current goal is (HxAB U HU HxU ) .
Apply HABne to the current goal.
Let y be given.
We prove the intermediate
claim HyU :
y ∈ U .
An
exact proof term for the current goal is
(binintersectE1 U (A ∩ B ) y Hy ) .
We prove the intermediate
claim HyAB :
y ∈ A ∩ B .
An
exact proof term for the current goal is
(binintersectE2 U (A ∩ B ) y Hy ) .
We prove the intermediate
claim HyB :
y ∈ B .
An
exact proof term for the current goal is
(binintersectE2 A B y HyAB ) .
We prove the intermediate
claim HyUB :
y ∈ U ∩ B .
An exact proof term for the current goal is HyU .
An exact proof term for the current goal is HyB .
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUB .
An
exact proof term for the current goal is
(SepI X (λx0 ⇒ ∀U : set , U ∈ Tx → x0 ∈ U → U ∩ B ≠ Empty ) x HxX (andER (x ∈ X ) (∀U : set , U ∈ Tx → x ∈ U → U ∩ B ≠ Empty ) HxB ) ) .
∎
Proof: Let X, Y, Tx, Ty, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
We prove the intermediate
claim HYsubX :
Y ⊆ X .
The rest of this subproof is missing.
Apply andI to the current goal.
An exact proof term for the current goal is HTy .
Let y1 and y2 be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and seq be given.
Let x be given.
Let U be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
Apply andI to the current goal.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X be given.
We prove the intermediate
claim HXE :
X ∖ Empty = X .
Let x be given.
An exact proof term for the current goal is Hx .
An
exact proof term for the current goal is
(EmptyE x Hfalse ) .
rewrite the current goal using HXE (from left to right).
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty, Z, Tz, f and g be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty, Z, Tz, f and g be given.
∎
Proof: Let X, Tx, Y, Ty, f and A be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, A, B, Y, Tx, Ty, f and g be given.
The rest of this subproof is missing.
∎
Proof: Let A, X, Tx, Y, Ty, f and g be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Definition. We define
open_ball to be
λX d x ⇒ { y ∈ X | ∃r ∈ R , Rlt (d x y ) r } of type
set → set → set → set .
Proof: Let X and d be given.
The rest of this subproof is missing.
∎
Proof: Let X and d be given.
The rest of this subproof is missing.
∎
Proof: Let X and d be given.
The rest of this subproof is missing.
∎
Proof: Let X, dX, Y, dY and f be given.
The rest of this subproof is missing.
∎
Definition. We define
sequence_in to be
λseq A ⇒ seq ⊆ A of type
set → set → prop .
Definition. We define
image_of to be
λf seq ⇒ Repl seq (λy ⇒ y ) of type
set → set → set .
Proof: Let X, d, seq, x and y be given.
The rest of this subproof is missing.
∎
Proof: Let X, dX, Y, dY, f_seq and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, d, seq and x be given.
An exact proof term for the current goal is H .
∎
Proof: Let X, dX, Y, dY and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, C, D and Y be given.
We will
prove Y ⊆ C ∨ Y ⊆ D .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and F be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and b be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let A be given.
Let x, y and z be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
covers to be
λX U ⇒ ∀x : set , x ∈ X → ∃u : set , u ∈ U ∧ x ∈ u of type
set → set → prop .
Proof: Let X and Tx be given.
Let x be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Let x be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Let x be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and f be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and U be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and x be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
Let x0 be given.
Let N be given.
The rest of this subproof is missing.
∎
Definition. We define
Abs to be
abs_SNo of type
set → set .
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and Ty be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let A be given.
The rest of this subproof is missing.
∎
Proof: Let A be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
directed_set to be
λJ ⇒ J ≠ Empty ∧ ∀i j : set , i ∈ J → j ∈ J → ∃k : set , k ∈ J of type
set → prop .
Proof: Let J be given.
An exact proof term for the current goal is H .
∎
Proof: Let J and K be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, net, sub and x be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and x be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, net and x be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
open_cover to be
λX Tx U ⇒ (∀u : set , u ∈ U → u ∈ Tx ) ∧ covers X U of type
set → set → set → prop .
Proof: Let X, Tx, A and x be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let n be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
dense_in to be
λA X Tx ⇒ closure_of X Tx A = X of type
set → set → set → prop .
Proof: Let X and Tx be given.
Let U be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
R_K to be
R of type
set .
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X and d be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let J be given.
The rest of this subproof is missing.
∎
Definition. We define
S_Omega to be
ω of type
set .
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A, B, a and b be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Let F and J be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A, a, b and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and U be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let I and Xi be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Definition. We define
refine_of to be
λV U ⇒ ∀v : set , v ∈ V → ∃u : set , u ∈ U ∧ v ⊆ u of type
set → set → prop .
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and U be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, d, seq and x be given.
The rest of this subproof is missing.
∎
Proof: Let k be given.
The rest of this subproof is missing.
∎
Proof: Let X and J be given.
Let seq and x be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and d be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and F be given.
The rest of this subproof is missing.
∎
Proof: Let Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and d be given.
Assume Hcomp .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hcomp HHaus .
The rest of this subproof is missing.
∎
Proof: Let X be given.
Assume HBaire .
Let U be given.
Assume Hopen .
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X be given.
We use
Empty to
witness the existential quantifier.
The rest of this subproof is missing.
∎
Proof: Let X and n be given.
Assume Hcomp .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hman Hcomp .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hcomp Hmet Hdim .
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y and n be given.
Assume HX HY .
The rest of this subproof is missing.
∎
Proof: Let X, Y, Z and n be given.
Assume HY HZ .
Apply HY to the current goal.
Assume Hn HTy .
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
The rest of this subproof is missing.
∎
Proof: Let X, Fam and n be given.
Assume Hfin Hall .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hcomp Hman .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hcomp Hman .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Harc .
Apply Harc to the current goal.
Let f be given.
Assume Hhom .
The rest of this subproof is missing.
∎
Proof: Let G and Tg be given.
Assume Hlin .
The rest of this subproof is missing.
∎
Definition. We define
affine_plane to be
λS ⇒ { x ∈ R | ∃tcoeffs : set , (∀s : set , s ∈ S → ∃t : set , t ∈ R ∧ (s ,t ) ∈ tcoeffs ) ∧ True } of type
set → set .
Proof: Let N, pts and delta be given.
Assume HN Hfin Hpts Hdelta .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hcomp Hmet Hdim Hm .
The rest of this subproof is missing.
∎
Proof: Let X and N be given.
Assume HN Hcomp Hsub .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hcomp Hman .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hcomp Hman .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume HTxdisc HTxtop .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hconn HT1 Hdist Hdim0 .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume HX .
The rest of this subproof is missing.
∎
Proof: Let zero, e1, e2, e3 and ones be given.
Assume Hz He1 He2 He3 Hones .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hdim Hcomp Hmet .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hlc HHaus Hsec Hdim .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hman .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hsig HHaus Hdim .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hm Hman .
The rest of this subproof is missing.
∎
Proof: Let X and N be given.
Assume HN Hsub Hclosed .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc Hcomp HHaus .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc Hman .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hmet .
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Assume Hnorm .
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let Tdict be given.
Assume HTdict .
The rest of this subproof is missing.
∎
Proof: Let L and TL be given.
Assume HL HTL .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and m be given.
Assume Hloc Hmet .
Let C be given.
Assume HC .
The rest of this subproof is missing.
∎
Definition. We define
linear_continuum to be
λX Tx ⇒ ∃less : set → set → prop , Tx = order_topology X ∧ (∀A : set , A ⊆ X → A ≠ Empty → (∃upper : set , upper ∈ X ∧ ∀a : set , a ∈ A → less a upper ) → ∃lub : set , lub ∈ X ∧ (∀a : set , a ∈ A → less a lub ∨ a = lub ) ∧ (∀bound : set , bound ∈ X → (∀a : set , a ∈ A → less a bound ∨ a = bound ) → less lub bound ∨ lub = bound ) ) of type
set → set → prop .
Proof: Let X, Tx and x be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Basis be given.
We will
prove ∃CountableSub : set , CountableSub ⊆ Basis ∧ countable CountableSub ∧ basis_on X CountableSub .
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and d be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let Tx be given.
The rest of this subproof is missing.
∎
Proof: Let Tx_SO and Tx_SbarO be given.
The rest of this subproof is missing.
∎
Proof: Let Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let Idx and Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and f be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Let Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty, Idx and Fam be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let J be given.
Let Fam be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let G and Tg be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, x and y be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Tx' be given.
Apply and3I to the current goal.
The rest of this subproof is missing.
The rest of this subproof is missing.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty, f and g be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and p be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, Y, Ty and p be given.
The rest of this subproof is missing.
∎
Proof: Let G, Tg, X, Tx and alpha be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
The rest of this subproof is missing.
∎
Proof: Let Idx and Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
Apply iffI to the current goal.
Let A and B be given.
Apply H1 to the current goal.
Assume Hnorm Hsep .
An exact proof term for the current goal is Hsep A B H2 .
Apply andI to the current goal.
The rest of this subproof is missing.
An exact proof term for the current goal is H1 .
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let J be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A, B and U be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, d, A and B be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and A be given.
Apply iffI to the current goal.
The rest of this subproof is missing.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
Apply iffI to the current goal.
The rest of this subproof is missing.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx, A and B be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let G and Tg be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Fam be given.
The rest of this subproof is missing.
∎
Proof: Let Fam be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X and Tx be given.
The rest of this subproof is missing.
∎
Proof: Let X, Tx and Y be given.
The rest of this subproof is missing.
∎
Proof:
The rest of this subproof is missing.
∎
Proof: Let f be given.
The rest of this subproof is missing.
∎
Proof: Let D be given.
The rest of this subproof is missing.
∎
Proof: Let D be given.
The rest of this subproof is missing.
∎
Proof: Let fn and f be given.
The rest of this subproof is missing.
∎
Proof: Let g and f be given.
Let x be given.
The rest of this subproof is missing.
∎
Proof: Let X, d and FF be given.
The rest of this subproof is missing.
∎
Proof: Let Tl be given.
The rest of this subproof is missing.
∎
Proof: Let f, g and k be given.
The rest of this subproof is missing.
∎
Proof: Let n and eps be given.
The rest of this subproof is missing.
∎